:: CALCUL_2 semantic presentation

definition
let c1, c2 be natural number ;
func seq c1,c2 -> set equals :: CALCUL_2:def 1
{ b1 where B is Nat : ( 1 + a1 <= b1 & b1 <= a2 + a1 ) } ;
coherence
{ b1 where B is Nat : ( 1 + c1 <= b1 & b1 <= c2 + c1 ) } is set ;
end;

:: deftheorem defines seq CALCUL_2:def 1 :
for b1, b2 being natural number holds seq b1,b2 = { b3 where B is Nat : ( 1 + b1 <= b3 & b3 <= b2 + b1 ) } ;

definition
let c1, c2 be natural number ;
redefine func seq as seq c1,c2 -> Subset of NAT ;
coherence
seq c1,c2 is Subset of NAT
proof
set c3 = seq c1,c2;
seq c1,c2 c= NAT
proof
let c4 be set ; :: according to TARSKI:def 3
assume c4 in seq c1,c2 ;
then c4 in { b1 where B is Nat : ( 1 + c1 <= b1 & b1 <= c2 + c1 ) } ;
then ex b1 being Nat st
( c4 = b1 & 1 + c1 <= b1 & b1 <= c2 + c1 ) ;
hence c4 in NAT ;
end;
hence seq c1,c2 is Subset of NAT ;
end;
end;

theorem E1: :: CALCUL_2:1
for b1, b2, b3 being natural number holds
( b1 in seq b2,b3 iff ( 1 + b2 <= b1 & b1 <= b3 + b2 ) )
proof
let c1, c2, c3 be natural number ;
E2: c1 is Nat by ORDINAL2:def 21;
( c1 in { b1 where B is Nat : ( 1 + c2 <= b1 & b1 <= c3 + c2 ) } iff ex b1 being Nat st
( c1 = b1 & 1 + c2 <= b1 & b1 <= c3 + c2 ) ) ;
hence ( c1 in seq c2,c3 iff ( 1 + c2 <= c1 & c1 <= c3 + c2 ) ) by E2;
end;

theorem E2: :: CALCUL_2:2
for b1 being natural number holds seq b1,0 = {}
proof
let c1 be natural number ;
hereby
consider c2 being Element of seq c1,0;
assume E3: seq c1,0 <> {} ;
then reconsider c3 = c2 as Nat by TARSKI:def 3;
( 1 + c1 <= c3 & c3 <= 0 + c1 ) by E3, E1;
hence not verum by NAT_1:38;
end;
end;

theorem E3: :: CALCUL_2:3
for b1, b2 being natural number holds
( b1 = 0 or b1 + b2 in seq b2,b1 )
proof
let c1, c2 be natural number ;
assume c1 <> 0 ;
then consider c3 being Nat such that
E4: c1 = c3 + 1 by NAT_1:22;
E5: c1 + c2 is Nat by ORDINAL2:def 21;
1 <= c1 by E4, NAT_1:29;
then ( 1 + c2 <= c1 + c2 & c1 + c2 <= c1 + c2 ) by XREAL_1:8;
then c1 + c2 in { b1 where B is Nat : ( 1 + c2 <= b1 & b1 <= c1 + c2 ) } by E5;
hence c1 + c2 in seq c2,c1 ;
end;

theorem E4: :: CALCUL_2:4
for b1, b2, b3 being natural number holds
( b1 <= b2 iff seq b3,b1 c= seq b3,b2 )
proof
let c1, c2, c3 be natural number ;
thus ( c1 <= c2 implies seq c3,c1 c= seq c3,c2 )
proof
assume E5: c1 <= c2 ;
let c4 be set ; :: according to TARSKI:def 3
assume E6: c4 in seq c3,c1 ;
reconsider c5 = c4 as Nat by E6;
E7: ( 1 + c3 <= c5 & c5 <= c1 + c3 ) by E6, E1;
c1 + c3 <= c2 + c3 by E5, XREAL_1:8;
then c5 <= c2 + c3 by E7, XXREAL_0:2;
then c4 in { b1 where B is Nat : ( 1 + c3 <= b1 & b1 <= c2 + c3 ) } by E7;
hence c4 in seq c3,c2 ;
end;
assume E5: seq c3,c1 c= seq c3,c2 ;
now
assume c1 <> 0 ;
then c1 + c3 in seq c3,c1 by E3;
then c1 + c3 <= c2 + c3 by E5, E1;
hence c1 <= c2 by XREAL_1:8;
end;
hence c1 <= c2 ;
end;

theorem E5: :: CALCUL_2:5
for b1, b2 being natural number holds (seq b1,b2) \/ {((b1 + b2) + 1)} = seq b1,(b2 + 1)
proof
let c1, c2 be natural number ;
thus (seq c1,c2) \/ {((c1 + c2) + 1)} c= seq c1,(c2 + 1) :: according to XBOOLE_0:def 10
proof
c2 + 0 <= c2 + 1 by XREAL_1:9;
then E6: seq c1,c2 c= seq c1,(c2 + 1) by E4;
let c3 be set ; :: according to TARSKI:def 3
assume E7: c3 in (seq c1,c2) \/ {((c1 + c2) + 1)} ;
( c3 in seq c1,c2 or c3 in {((c1 + c2) + 1)} ) by E7, XBOOLE_0:def 2;
then ( c3 in seq c1,(c2 + 1) or c3 = c1 + (c2 + 1) ) by E6, TARSKI:def 1;
hence c3 in seq c1,(c2 + 1) by E3;
end;
let c3 be set ; :: according to TARSKI:def 3
assume E6: c3 in seq c1,(c2 + 1) ;
reconsider c4 = c3 as Nat by E6;
( 1 + c1 <= c4 & c4 <= (c2 + 1) + c1 ) by E6, E1;
then ( 1 + c1 <= c4 & ( c4 <= c1 + c2 or c4 = (c1 + c2) + 1 ) ) by NAT_1:26;
then ( c4 in seq c1,c2 or c4 in {((c1 + c2) + 1)} ) by TARSKI:def 1;
hence c3 in (seq c1,c2) \/ {((c1 + c2) + 1)} by XBOOLE_0:def 2;
end;

theorem E6: :: CALCUL_2:6
for b1, b2 being Nat holds seq b1,b2,b2 are_equipotent
proof
let c1, c2 be Nat;
defpred S1[ Nat] means seq c1,a1,a1 are_equipotent ;
E7: S1[0] by E2;
E8: for b1 being Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c3 be Nat;
assume E9: seq c1,c3,c3 are_equipotent ;
reconsider c4 = c1 + c3 as Nat ;
E10: seq c1,(c3 + 1) = (seq c1,c3) \/ {(c4 + 1)} by E5;
E11: c3 + 1 = succ c3 by CARD_1:52
.= c3 \/ {c3} by ORDINAL1:def 1 ;
E12: {(c4 + 1)},{c3} are_equipotent by CARD_1:48;
E13: now
assume c3 meets {c3} ;
then consider c5 being set such that
E14: ( c5 in c3 & c5 in {c3} ) by XBOOLE_0:3;
c5 = c3 by E14, TARSKI:def 1;
hence not verum by E14;
end;
now
assume seq c1,c3 meets {(c4 + 1)} ;
then consider c5 being set such that
E14: ( c5 in seq c1,c3 & c5 in {(c4 + 1)} ) by XBOOLE_0:3;
E15: ( c5 = c4 + 1 & c3 + c1 <= c4 ) by E14, TARSKI:def 1;
not c4 + 1 <= c4 by NAT_1:38;
hence not verum by E14, E15, E1;
end;
hence S1[c3 + 1] by E9, E10, E11, E12, E13, CARD_1:58;
end;
for b1 being Nat holds
S1[b1] from NAT_1:sch 1(E7, E8);
 hence seq c1,c2,c2 are_equipotent ;
end;

registration
let c1, c2 be Nat;
cluster seq a1,a2 -> finite ;
coherence
seq c1,c2 is finite
proof
E7: c2 is finite by CARD_1:69;
c2, seq c1,c2 are_equipotent by E6;
hence seq c1,c2 is finite by E7, CARD_1:68;
end;
end;

registration
let c1 be FinSequence of CQC-WFF ;
cluster Card a1 -> finite ;
coherence
len c1 is finite by CARD_1:69;
end;

theorem E7: :: CALCUL_2:7
for b1, b2 being Nat holds seq b1,b2 c= Seg (b1 + b2)
proof
let c1, c2 be Nat;
let c3 be set ; :: according to TARSKI:def 3
assume E8: c3 in seq c1,c2 ;
then reconsider c4 = c3 as Nat ;
E9: ( 1 + c1 <= c4 & c4 <= c2 + c1 ) by E8, E1;
1 <= 1 + c1 by NAT_1:29;
then 1 <= c4 by E9, XXREAL_0:2;
hence c3 in Seg (c1 + c2) by E9, FINSEQ_1:3;
end;

theorem :: CALCUL_2:8
for b1, b2 being Nat holds Seg b1 misses seq b1,b2
proof
let c1, c2 be Nat;
assume Seg c1 meets seq c1,c2 ;
then consider c3 being set such that
E8: ( c3 in Seg c1 & c3 in seq c1,c2 ) by XBOOLE_0:3;
reconsider c4 = c3 as Nat by E8;
( c4 <= c1 & c1 + 1 <= c4 ) by E8, E1, FINSEQ_1:3;
hence not verum by NAT_1:38;
end;

theorem :: CALCUL_2:9
for b1, b2 being FinSequence holds Seg (len (b1 ^ b2)) = (Seg (len b1)) \/ (seq (len b1),(len b2))
proof
let c1, c2 be FinSequence;
now
let c3 be set ;
assume E8: c3 in Seg (len (c1 ^ c2)) ;
reconsider c4 = c3 as Nat by E8;
E9: ( 1 <= c4 & c4 <= len (c1 ^ c2) ) by E8, FINSEQ_1:3;
E10: now
assume c4 <= len c1 ;
then E11: c4 in Seg (len c1) by E9, FINSEQ_1:3;
Seg (len c1) c= (Seg (len c1)) \/ (seq (len c1),(len c2)) by XBOOLE_1:7;
hence c3 in (Seg (len c1)) \/ (seq (len c1),(len c2)) by E11;
end;
now
assume len c1 < c4 ;
then ( (len c1) + 1 <= c4 & c4 <= (len c1) + (len c2) ) by E9, FINSEQ_1:35, NAT_1:38;
then E11: c3 in seq (len c1),(len c2) ;
seq (len c1),(len c2) c= (Seg (len c1)) \/ (seq (len c1),(len c2)) by XBOOLE_1:7;
hence c3 in (Seg (len c1)) \/ (seq (len c1),(len c2)) by E11;
end;
hence c3 in (Seg (len c1)) \/ (seq (len c1),(len c2)) by E10;
end;
hence Seg (len (c1 ^ c2)) c= (Seg (len c1)) \/ (seq (len c1),(len c2)) by TARSKI:def 3; :: according to XBOOLE_0:def 10
let c3 be set ; :: according to TARSKI:def 3
assume E8: c3 in (Seg (len c1)) \/ (seq (len c1),(len c2)) ;
E9: now
assume E10: c3 in Seg (len c1) ;
then reconsider c4 = c3 as Nat ;
E11: ( 1 <= c4 & c4 <= len c1 ) by E10, FINSEQ_1:3;
len c1 <= len (c1 ^ c2) by CALCUL_1:6;
then c4 <= len (c1 ^ c2) by E11, XXREAL_0:2;
hence c3 in Seg (len (c1 ^ c2)) by E11, FINSEQ_1:3;
end;
now
assume E10: c3 in seq (len c1),(len c2) ;
then reconsider c4 = c3 as Nat ;
E11: ( 1 + (len c1) <= c4 & c4 <= (len c2) + (len c1) ) by E10, E1;
then E12: c4 <= len (c1 ^ c2) by FINSEQ_1:35;
1 <= 1 + (len c1) by NAT_1:29;
then 1 <= c4 by E11, XXREAL_0:2;
hence c3 in Seg (len (c1 ^ c2)) by E12, FINSEQ_1:3;
end;
hence c3 in Seg (len (c1 ^ c2)) by E8, E9, XBOOLE_0:def 2;
end;

theorem E8: :: CALCUL_2:10
for b1, b2 being FinSequence of CQC-WFF holds len (Sgm (seq (len b1),(len b2))) = len b2
proof
let c1, c2 be FinSequence of CQC-WFF ;
seq (len c1),(len c2), len c2 are_equipotent by E6;
then card (seq (len c1),(len c2)) = card (len c2) by CARD_1:81;
then E9: card (seq (len c1),(len c2)) = len c2 by FINSEQ_1:78;
seq (len c1),(len c2) c= Seg ((len c1) + (len c2)) by E7;
hence len (Sgm (seq (len c1),(len c2))) = len c2 by E9, FINSEQ_3:44;
end;

theorem E9: :: CALCUL_2:11
for b1, b2 being FinSequence of CQC-WFF holds dom (Sgm (seq (len b1),(len b2))) = dom b2
proof
let c1, c2 be FinSequence of CQC-WFF ;
len (Sgm (seq (len c1),(len c2))) = len c2 by E8;
hence dom (Sgm (seq (len c1),(len c2))) = dom c2 by FINSEQ_3:31;
end;

theorem E10: :: CALCUL_2:12
for b1, b2 being FinSequence of CQC-WFF holds rng (Sgm (seq (len b1),(len b2))) = seq (len b1),(len b2)
proof
let c1, c2 be FinSequence of CQC-WFF ;
seq (len c1),(len c2) c= Seg ((len c1) + (len c2)) by E7;
hence rng (Sgm (seq (len c1),(len c2))) = seq (len c1),(len c2) by FINSEQ_1:def 13;
end;

theorem E11: :: CALCUL_2:13
for b1 being Nat
for b2, b3 being FinSequence of CQC-WFF holds
( b1 in dom (Sgm (seq (len b2),(len b3))) implies (Sgm (seq (len b2),(len b3))) . b1 = (len b2) + b1 )
proof
let c1 be Nat;
let c2, c3 be FinSequence of CQC-WFF ;
assume c1 in dom (Sgm (seq (len c2),(len c3))) ;
then c1 in dom c3 by E9;
then E12: ( 1 <= c1 & c1 <= len c3 ) by FINSEQ_3:27;
defpred S1[ Nat] means ( ( 1 <= a1 & a1 <= len c3 ) implies ( ( for b1 being Nat holds
( ( 1 <= b1 & b1 <= a1 ) implies ( (Sgm (seq (len c2),(len c3))) . b1 = (len c2) + b1 ) ) ) ) );
E13: S1[0] ;
E14: for b1 being Nat holds
( S1[b1] implies S1[b1 + 1] )
proof
let c4 be Nat;
assume E15: S1[c4] ;
assume E16: ( 1 <= c4 + 1 & c4 + 1 <= len c3 ) ;
let c5 be Nat;
assume E17: ( 1 <= c5 & c5 <= c4 + 1 ) ;
E18: ( c5 <= c4 implies (Sgm (seq (len c2),(len c3))) . c5 = (len c2) + c5 ) by E15, E16, E17, XXREAL_0:2, NAT_1:38;
now
assume E19: c5 = c4 + 1 ;
dom (Sgm (seq (len c2),(len c3))) = dom c3 by E9;
then c5 in dom (Sgm (seq (len c2),(len c3))) by E16, E19, FINSEQ_3:27;
then (Sgm (seq (len c2),(len c3))) . c5 in rng (Sgm (seq (len c2),(len c3))) by FUNCT_1:12;
then reconsider c6 = (Sgm (seq (len c2),(len c3))) . c5 as Nat ;
E20: now
assume E21: c6 < (len c2) + (c4 + 1) ;
E22: now
assume E23: c4 = 0 ;
then not c6 in seq (len c2),(len c3) by E21, E1;
then E24: not c6 in rng (Sgm (seq (len c2),(len c3))) by E10;
1 <= len c3 by E16, XXREAL_0:2;
then 1 in dom c3 by FINSEQ_3:27;
then 1 in dom (Sgm (seq (len c2),(len c3))) by E9;
hence not verum by E19, E23, E24, FUNCT_1:12;
end;
now
assume E23: c4 <> 0 ;
E24: c6 < ((len c2) + c4) + 1 by E21;
0 < c4 by E23;
then E25: ( 0 + 1 <= c4 & c4 <= c4 + 1 ) by NAT_1:38;
E26: (Sgm (seq (len c2),(len c3))) . c4 = (len c2) + c4 by E15, E16, E25, XXREAL_0:2;
then reconsider c7 = (Sgm (seq (len c2),(len c3))) . c4 as Nat ;
E27: ( 1 <= c4 & c4 < c4 + 1 & c4 + 1 <= len (Sgm (seq (len c2),(len c3))) ) by E16, E25, E8, NAT_1:38;
( c6 <= c7 & seq (len c2),(len c3) c= Seg ((len c2) + (len c3)) ) by E24, E26, E7, NAT_1:38;
hence not verum by E19, E27, FINSEQ_1:def 13;
end;
hence not verum by E22;
end;
now
assume E21: c6 > (len c2) + (c4 + 1) ;
E22: 1 + (len c2) <= (1 + (len c2)) + c4 by NAT_1:29;
(len c2) + (c4 + 1) <= (len c3) + (len c2) by E16, XREAL_1:8;
then (len c2) + (c4 + 1) in seq (len c2),(len c3) by E22;
then (len c2) + (c4 + 1) in rng (Sgm (seq (len c2),(len c3))) by E10;
then consider c7 being Nat such that
E23: ( c7 in dom (Sgm (seq (len c2),(len c3))) & (Sgm (seq (len c2),(len c3))) . c7 = (len c2) + (c4 + 1) ) by FINSEQ_2:11;
E24: now
assume E25: c7 <= c4 + 1 ;
now
assume E26: c7 <= c4 ;
then E27: c7 < c4 + 1 by NAT_1:38;
now
assume 1 <= c7 ;
then (len c2) + (c4 + 1) = (len c2) + c7 by E15, E16, E23, E26, XXREAL_0:2, NAT_1:38;
hence not verum by E27;
end;
hence not verum by E23, FINSEQ_3:27;
end;
hence not verum by E19, E21, E23, E25, NAT_1:26;
end;
reconsider c8 = (Sgm (seq (len c2),(len c3))) . c7 as Nat by E23;
E25: ( 1 <= c5 & c5 < c7 & c7 <= len (Sgm (seq (len c2),(len c3))) ) by E19, E23, E24, FINSEQ_3:27, NAT_1:29;
seq (len c2),(len c3) c= Seg ((len c2) + (len c3)) by E7;
hence not verum by E21, E23, E25, FINSEQ_1:def 13;
end;
hence (Sgm (seq (len c2),(len c3))) . c5 = (len c2) + c5 by E19, E20, XXREAL_0:1;
end;
hence (Sgm (seq (len c2),(len c3))) . c5 = (len c2) + c5 by E17, E18, NAT_1:26;
end;
for b1 being Nat holds
S1[b1] from NAT_1:sch 1(E13, E14);
 hence (Sgm (seq (len c2),(len c3))) . c1 = (len c2) + c1 by E12;
end;

theorem E12: :: CALCUL_2:14
for b1, b2 being FinSequence of CQC-WFF holds seq (len b1),(len b2) c= dom (b1 ^ b2)
proof
let c1, c2 be FinSequence of CQC-WFF ;
now
let c3 be set ;
assume E13: c3 in seq (len c1),(len c2) ;
reconsider c4 = c3 as Nat by E13;
E14: ( 1 + (len c1) <= c4 & c4 <= (len c2) + (len c1) ) by E13, E1;
1 <= 1 + (len c1) by NAT_1:29;
then ( 1 <= c4 & c4 <= len (c1 ^ c2) ) by E14, XXREAL_0:2, FINSEQ_1:35;
hence c3 in dom (c1 ^ c2) by FINSEQ_3:27;
end;
hence seq (len c1),(len c2) c= dom (c1 ^ c2) by TARSKI:def 3;
end;

theorem E13: :: CALCUL_2:15
for b1, b2 being FinSequence of CQC-WFF holds dom ((b1 ^ b2) | (seq (len b1),(len b2))) = seq (len b1),(len b2)
proof
let c1, c2 be FinSequence of CQC-WFF ;
E14: dom ((c1 ^ c2) | (seq (len c1),(len c2))) = (dom (c1 ^ c2)) /\ (seq (len c1),(len c2)) by RELAT_1:90;
seq (len c1),(len c2) c= dom (c1 ^ c2) by E12;
hence dom ((c1 ^ c2) | (seq (len c1),(len c2))) = seq (len c1),(len c2) by E14, XBOOLE_1:28;
end;

theorem E14: :: CALCUL_2:16
for b1, b2 being FinSequence of CQC-WFF holds Seq ((b1 ^ b2) | (seq (len b1),(len b2))) = (Sgm (seq (len b1),(len b2))) * (b1 ^ b2)
proof
let c1, c2 be FinSequence of CQC-WFF ;
reconsider c3 = (c1 ^ c2) | (seq (len c1),(len c2)) as FinSubsequence ;
Seq c3 = c3 * (Sgm (dom c3)) by FINSEQ_1:def 14
.= c3 * (Sgm (seq (len c1),(len c2))) by E13
.= ((c1 ^ c2) | (rng (Sgm (seq (len c1),(len c2))))) * (Sgm (seq (len c1),(len c2))) by E10
.= (c1 ^ c2) * (Sgm (seq (len c1),(len c2))) by FUNCT_4:2 ;
hence Seq ((c1 ^ c2) | (seq (len c1),(len c2))) = (Sgm (seq (len c1),(len c2))) * (c1 ^ c2) ;
end;

theorem E15: :: CALCUL_2:17
for b1, b2 being FinSequence of CQC-WFF holds dom (Seq ((b1 ^ b2) | (seq (len b1),(len b2)))) = dom b2
proof
let c1, c2 be FinSequence of CQC-WFF ;
rng (Sgm (seq (len c1),(len c2))) = seq (len c1),(len c2) by E10;
then E16: rng (Sgm (seq (len c1),(len c2))) c= dom (c1 ^ c2) by E12;
dom (Seq ((c1 ^ c2) | (seq (len c1),(len c2)))) = dom ((Sgm (seq (len c1),(len c2))) * (c1 ^ c2)) by E14;
then dom (Seq ((c1 ^ c2) | (seq (len c1),(len c2)))) = dom (Sgm (seq (len c1),(len c2))) by E16, RELAT_1:46;
hence dom (Seq ((c1 ^ c2) | (seq (len c1),(len c2)))) = dom c2 by E9;
end;

theorem E16: :: CALCUL_2:18
for b1, b2 being FinSequence of CQC-WFF holds b1 is_Subsequence_of b2 ^ b1
proof
let c1, c2 be FinSequence of CQC-WFF ;
E17: for b1 being Nat holds
( b1 in dom (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) implies (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) . b1 = c1 . b1 )
proof
let c3 be Nat;
assume E18: c3 in dom (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) ;
E19: (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) . c3 = ((Sgm (seq (len c2),(len c1))) * (c2 ^ c1)) . c3 by E14;
E20: c3 in dom c1 by E18, E15;
then E21: c3 in dom (Sgm (seq (len c2),(len c1))) by E9;
then (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) . c3 = (c2 ^ c1) . ((Sgm (seq (len c2),(len c1))) . c3) by E19, FUNCT_1:23;
then (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) . c3 = (c2 ^ c1) . ((len c2) + c3) by E21, E11;
hence (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) . c3 = c1 . c3 by E20, FINSEQ_1:def 7;
end;
dom (Seq ((c2 ^ c1) | (seq (len c2),(len c1)))) = dom c1 by E15;
then Seq ((c2 ^ c1) | (seq (len c2),(len c1))) = c1 by E17, FINSEQ_1:17;
hence c1 is_Subsequence_of c2 ^ c1 by CALCUL_1:def 4;
end;

definition
let c1 be non empty set ;
let c2 be FinSequence of c1;
let c3 be Permutation of dom c2;
func Per c2,c3 -> FinSequence of a1 equals :: CALCUL_2:def 2
a3 * a2;
coherence
c3 * c2 is FinSequence of c1
proof
c3 is onto by FUNCT_2:def 4;
then E17: rng c3 = dom c2 by FUNCT_2:def 3;
then dom (c3 * c2) = dom c3 by RELAT_1:46;
then dom (c3 * c2) = dom c2 by FUNCT_2:67;
then consider c4 being Nat such that
E18: dom (c3 * c2) = Seg c4 by FINSEQ_1:def 2;
reconsider c5 = c3 * c2 as FinSequence by E18, FINSEQ_1:def 2;
rng c5 = rng c2 by E17, RELAT_1:47;
hence c3 * c2 is FinSequence of c1 by FINSEQ_1:def 4;
end;
end;

:: deftheorem defines Per CALCUL_2:def 2 :
for b1 being non empty set
for b2 being FinSequence of b1
for b3 being Permutation of dom b2 holds Per b2,b3 = b3 * b2;

theorem E17: :: CALCUL_2:19
for b1 being FinSequence of CQC-WFF
for b2 being Permutation of dom b1 holds dom (Per b1,b2) = dom b1
proof
let c1 be FinSequence of CQC-WFF ;
let c2 be Permutation of dom c1;
c2 is onto by FUNCT_2:def 4;
then rng c2 = dom c1 by FUNCT_2:def 3;
then dom (c2 * c1) = dom c2 by RELAT_1:46;
then dom (c2 * c1) = dom c1 by FUNCT_2:67;
hence dom (Per c1,c2) = dom c1 ;
end;

theorem E18: :: CALCUL_2:20
for b1 being Element of CQC-WFF
for b2, b3 being FinSequence of CQC-WFF holds
( |- b2 ^ <*b1*> implies |- (b3 ^ b2) ^ <*b1*> )
proof
let c1 be Element of CQC-WFF ;
let c2, c3 be FinSequence of CQC-WFF ;
assume E19: |- c2 ^ <*c1*> ;
E20: ( Ant (c2 ^ <*c1*>) = c2 & Suc (c2 ^ <*c1*>) = c1 ) by CALCUL_1:5;
then Ant (c2 ^ <*c1*>) is_Subsequence_of c3 ^ c2 by E16;
then ( Ant (c2 ^ <*c1*>) is_Subsequence_of Ant ((c3 ^ c2) ^ <*c1*>) & Suc (c2 ^ <*c1*>) = Suc ((c3 ^ c2) ^ <*c1*>) ) by E20, CALCUL_1:5;
hence |- (c3 ^ c2) ^ <*c1*> by E19, CALCUL_1:36;
end;

definition
let c1 be FinSequence of CQC-WFF ;
func Begin c1 -> Element of CQC-WFF means :E19: :: CALCUL_2:def 3
a2 = a1 . 1 if 1 <= len a1
otherwise a2 = VERUM ;
existence
( not ( 1 <= len c1 & ( for b1 being Element of CQC-WFF holds
not b1 = c1 . 1 ) ) & not ( not 1 <= len c1 & ( for b1 being Element of CQC-WFF holds
not b1 = VERUM ) ) )
proof
E19: not ( 1 <= len c1 & ( for b1 being Element of CQC-WFF holds
not b1 = c1 . 1 ) )
proof
assume 1 <= len c1 ;
then 1 in dom c1 by FINSEQ_3:27;
then c1 . 1 in CQC-WFF by FINSEQ_2:13;
hence ex b1 being Element of CQC-WFF st b1 = c1 . 1 ;
end;
thus ( not ( 1 <= len c1 & ( for b1 being Element of CQC-WFF holds
not b1 = c1 . 1 ) ) & not ( not 1 <= len c1 & ( for b1 being Element of CQC-WFF holds
not b1 = VERUM ) ) ) by E19;
end;
uniqueness
for b1, b2 being Element of CQC-WFF holds
( ( ( 1 <= len c1 & b1 = c1 . 1 & b2 = c1 . 1 ) implies ( b1 = b2 ) ) & ( ( b1 = VERUM & b2 = VERUM ) implies ( 1 <= len c1 or b1 = b2 ) ) ) ;
consistency
for b1 being Element of CQC-WFF holds
verum ;
end;

:: deftheorem E19 defines Begin CALCUL_2:def 3 :
for b1 being FinSequence of CQC-WFF
for b2 being Element of CQC-WFF holds
( ( 1 <= len b1 implies ( b2 = Begin b1 iff b2 = b1 . 1 ) ) & ( not 1 <= len b1 implies ( b2 = Begin b1 iff b2 = VERUM ) ) );

definition