:: CALCUL_1 semantic presentation

registration
let c1 be FinSequence;
let c2 be set ;
cluster a1 | a2 -> FinSubsequence-like ;
coherence
c1 | c2 is FinSubsequence-like by FINSEQ_1:69;
end;

definition
let c1 be non empty set ;
let c2 be FinSequence of c1;
func Ant a2 -> FinSequence of a1 means :E1: :: CALCUL_1:def 1
for b1 being Nat holds
( len a2 = b1 + 1 implies a3 = a2 | (Seg b1) ) if len a2 > 0
otherwise a3 = {} ;
existence
( not ( len c2 > 0 & for b1 being FinSequence of c1 holds
ex b2 being Nat st
( len c2 = b2 + 1 & not b1 = c2 | (Seg b2) ) ) & not ( not len c2 > 0 & for b1 being FinSequence of c1 holds
not b1 = {} ) )
proof
E1: not ( len c2 > 0 & for b1 being FinSequence of c1 holds
ex b2 being Nat st
( len c2 = b2 + 1 & not b1 = c2 | (Seg b2) ) )
proof
assume len c2 > 0 ;
then consider c3 being Nat such that
E2: len c2 = c3 + 1 by NAT_1:22;
take c4 = c2 | (Seg c3);
reconsider c5 = c4 as FinSequence by FINSEQ_1:19;
now
let c6 be set ;
assume E3: c6 in rng c5 ;
rng c5 c= rng c2 by RELAT_1:99;
then c6 in rng c2 by E3;
hence c6 in c1 ;
end;
then rng c5 c= c1 by TARSKI:def 3;
then reconsider c6 = c5 as FinSequence of c1 by FINSEQ_1:def 4;
for b1 being Nat holds
( len c2 = b1 + 1 implies c6 = c2 | (Seg b1) ) by E2;
hence ( c4 is FinSequence of c1 & for b1 being Nat holds
( len c2 = b1 + 1 implies c4 = c2 | (Seg b1) ) ) ;
end;
not ( not len c2 > 0 & for b1 being FinSequence of c1 holds
not b1 = {} )
proof
assume not len c2 > 0 ;
take c3 = {} ;
thus ( c3 is Element of bool [:NAT ,c1:] & c3 is Relation of NAT ,c1 & c3 is FinSequence of c1 & c3 = {} ) by FINSEQ_1:29;
end;
hence ( not ( len c2 > 0 & for b1 being FinSequence of c1 holds
ex b2 being Nat st
( len c2 = b2 + 1 & not b1 = c2 | (Seg b2) ) ) & not ( not len c2 > 0 & for b1 being FinSequence of c1 holds
not b1 = {} ) ) by E1;
end;
uniqueness
for b1, b2 being FinSequence of c1 holds
( ( ( for b3 being Nat holds
( len c2 = b3 + 1 implies b1 = c2 | (Seg b3) ) & for b3 being Nat holds
( len c2 = b3 + 1 implies b2 = c2 | (Seg b3) ) ) implies ( not len c2 > 0 or b1 = b2 ) ) & ( ( not len c2 > 0 & b1 = {} & b2 = {} ) implies ( b1 = b2 ) ) )
proof
let c3, c4 be FinSequence of c1;
( ( for b1 being Nat holds
( len c2 = b1 + 1 implies c3 = c2 | (Seg b1) ) & for b1 being Nat holds
( len c2 = b1 + 1 implies c4 = c2 | (Seg b1) ) ) implies ( not len c2 > 0 or c3 = c4 ) )
proof
assume E1: ( len c2 > 0 & for b1 being Nat holds
( len c2 = b1 + 1 implies c3 = c2 | (Seg b1) ) & for b1 being Nat holds
( len c2 = b1 + 1 implies c4 = c2 | (Seg b1) ) ) ;
then consider c5 being Nat such that
E2: len c2 = c5 + 1 by NAT_1:22;
( c3 = c2 | (Seg c5) & c4 = c2 | (Seg c5) ) by E1, E2;
hence c3 = c4 ;
end;
hence ( ( ( for b1 being Nat holds
( len c2 = b1 + 1 implies c3 = c2 | (Seg b1) ) & for b1 being Nat holds
( len c2 = b1 + 1 implies c4 = c2 | (Seg b1) ) ) implies ( not len c2 > 0 or c3 = c4 ) ) & ( ( not len c2 > 0 & c3 = {} & c4 = {} ) implies ( c3 = c4 ) ) ) ;
end;
consistency
for b1 being FinSequence of c1 holds
verum ;
end;

:: deftheorem E1 defines Ant CALCUL_1:def 1 :
for b1 being non empty set
for b2, b3 being FinSequence of b1 holds
( ( len b2 > 0 implies ( b3 = Ant b2 iff for b4 being Nat holds
( len b2 = b4 + 1 implies b3 = b2 | (Seg b4) ) ) ) & ( not len b2 > 0 implies ( b3 = Ant b2 iff b3 = {} ) ) );

definition
let c1 be non empty set ;
let c2 be FinSequence of c1;
assume E2: len c2 > 0 ;
func Suc a2 -> Element of a1 equals :E2: :: CALCUL_1:def 2
a2 . (len a2);
coherence
c2 . (len c2) is Element of c1
proof
( 0 + 1 <= len c2 & len c2 <= len c2 ) by E2, NAT_1:38;
then len c2 in dom c2 by FINSEQ_3:27;
then c2 . (len c2) in rng c2 by FUNCT_1:12;
hence c2 . (len c2) is Element of c1 ;
end;
end;

:: deftheorem E2 defines Suc CALCUL_1:def 2 :
for b1 being non empty set
for b2 being FinSequence of b1 holds
( len b2 > 0 implies Suc b2 = b2 . (len b2) );

definition
let c1 be non empty set ;
let c2 be Element of c1;
let c3 be FinSequence of c1;
pred a2 is_tail_of a3 means :E3: :: CALCUL_1:def 3
ex b1 being Nat st
( b1 in dom a3 & a3 . b1 = a2 );
end;

:: deftheorem E3 defines is_tail_of CALCUL_1:def 3 :
for b1 being non empty set
for b2 being Element of b1
for b3 being FinSequence of b1 holds
( b2 is_tail_of b3 iff ex b4 being Nat st
( b4 in dom b3 & b3 . b4 = b2 ) );

definition
let c1, c2 be FinSequence of CQC-WFF ;
pred a1 is_Subsequence_of a2 means :E4: :: CALCUL_1:def 4
ex b1 being Subset of NAT st a1 c= Seq (a2 | b1);
end;

:: deftheorem E4 defines is_Subsequence_of CALCUL_1:def 4 :
for b1, b2 being FinSequence of CQC-WFF holds
( b1 is_Subsequence_of b2 iff ex b3 being Subset of NAT st b1 c= Seq (b2 | b3) );

theorem E5: :: CALCUL_1:1
for b1, b2 being FinSequence of CQC-WFF holds
( b1 is_Subsequence_of b2 implies ( rng b1 c= rng b2 & ex b3 being Subset of NAT st rng b1 c= rng (b2 | b3) ) )
proof
let c1, c2 be FinSequence of CQC-WFF ;
assume c1 is_Subsequence_of c2 ;
then consider c3 being Subset of NAT such that
E6: c1 c= Seq (c2 | c3) by E4;
E7: now
let c4 be set ;
assume E8: c4 in rng c1 ;
consider c5 being Nat such that
E9: ( c5 in dom c1 & c1 . c5 = c4 ) by E8, FINSEQ_2:11;
E10: dom c1 c= dom (Seq (c2 | c3)) by E6, RELAT_1:25;
[c5,(c1 . c5)] in c1 by E9, FUNCT_1:8;
then (Seq (c2 | c3)) . c5 = c4 by E6, E9, FUNCT_1:8;
then E11: c4 in rng (Seq (c2 | c3)) by E9, E10, FUNCT_1:12;
rng (Seq (c2 | c3)) = rng ((Sgm (dom (c2 | c3))) * (c2 | c3)) by FINSEQ_1:def 14;
then rng (Seq (c2 | c3)) c= rng (c2 | c3) by RELAT_1:45;
hence c4 in rng (c2 | c3) by E11;
end;
then E8: rng c1 c= rng (c2 | c3) by TARSKI:def 3;
rng (c2 | c3) c= rng c2 by RELAT_1:99;
hence rng c1 c= rng c2 by E8, XBOOLE_1:1;
take c3 ;
thus rng c1 c= rng (c2 | c3) by E7, TARSKI:def 3;
end;

theorem E6: :: CALCUL_1:2
for b1 being FinSequence of CQC-WFF holds
( len b1 > 0 implies ( (len (Ant b1)) + 1 = len b1 & len (Ant b1) < len b1 ) )
proof
let c1 be FinSequence of CQC-WFF ;
assume len c1 > 0 ;
then consider c2 being Nat such that
E7: len c1 = c2 + 1 by NAT_1:22;
Ant c1 = c1 | (Seg c2) by E7, E1;
then dom (Ant c1) = (dom c1) /\ (Seg c2) by FUNCT_1:68;
then Seg (len (Ant c1)) = (dom c1) /\ (Seg c2) by FINSEQ_1:def 3;
then E8: Seg (len (Ant c1)) = (Seg (len c1)) /\ (Seg c2) by FINSEQ_1:def 3;
c2 <= len c1 by E7, NAT_1:29;
then Seg c2 c= Seg (len c1) by FINSEQ_1:7;
then E9: Seg (len (Ant c1)) = Seg c2 by E8, XBOOLE_1:28;
then E10: len (Ant c1) = c2 by FINSEQ_1:8;
thus (len (Ant c1)) + 1 = len c1 by E7, E9, FINSEQ_1:8;
thus len (Ant c1) < len c1 by E7, E10, NAT_1:38;
end;

theorem E7: :: CALCUL_1:3
for b1 being FinSequence of CQC-WFF holds
( len b1 > 0 implies ( b1 = (Ant b1) ^ <*(Suc b1)*> & rng b1 = (rng (Ant b1)) \/ {(Suc b1)} ) )
proof
let c1 be FinSequence of CQC-WFF ;
assume E8: len c1 > 0 ;
then E9: len c1 = (len (Ant c1)) + 1 by E6;
then len c1 = (len (Ant c1)) + (len <*(Suc c1)*>) by FINSEQ_1:56;
then E10: len c1 = len ((Ant c1) ^ <*(Suc c1)*>) by FINSEQ_1:35;
E11: now
let c2 be Nat;
assume E12: c2 in Seg (len c1) ;
E13: ( 1 <= c2 & c2 <= (len (Ant c1)) + 1 ) by E9, E12, FINSEQ_1:3;
E14: now
assume c2 <= len (Ant c1) ;
then E15: c2 in dom (Ant c1) by E13, FINSEQ_3:27;
Ant c1 = c1 | (Seg (len (Ant c1))) by E9, E1;
then Ant c1 = c1 | (dom (Ant c1)) by FINSEQ_1:def 3;
then c1 . c2 = (Ant c1) . c2 by E15, FUNCT_1:72;
hence c1 . c2 = ((Ant c1) ^ <*(Suc c1)*>) . c2 by E15, FINSEQ_1:def 7;
end;
now
assume E15: c2 = (len (Ant c1)) + 1 ;
then c2 = len c1 by E8, E6;
then c1 . c2 = Suc c1 by E8, E2;
then E16: c1 . c2 = <*(Suc c1)*> . 1 by FINSEQ_1:57;
1 in Seg 1 by FINSEQ_1:3;
then 1 in dom <*(Suc c1)*> by FINSEQ_1:55;
hence c1 . c2 = ((Ant c1) ^ <*(Suc c1)*>) . c2 by E15, E16, FINSEQ_1:def 7;
end;
hence c1 . c2 = ((Ant c1) ^ <*(Suc c1)*>) . c2 by E13, E14, NAT_1:26;
end;
then c1 = (Ant c1) ^ <*(Suc c1)*> by E10, FINSEQ_2:10;
then rng c1 = (rng (Ant c1)) \/ (rng <*(Suc c1)*>) by FINSEQ_1:44;
hence ( c1 = (Ant c1) ^ <*(Suc c1)*> & rng c1 = (rng (Ant c1)) \/ {(Suc c1)} ) by E10, E11, FINSEQ_1:55, FINSEQ_2:10;
end;

theorem E8: :: CALCUL_1:4
for b1 being FinSequence of CQC-WFF holds
not ( len b1 > 1 & not len (Ant b1) > 0 )
proof
let c1 be FinSequence of CQC-WFF ;
assume E9: len c1 > 1 ;
then len c1 > 0 ;
then (len (Ant c1)) + 1 = len c1 by E6;
then (len (Ant c1)) + 1 > 1 by E9;
then 1 <= len (Ant c1) by NAT_1:38;
hence len (Ant c1) > 0 ;
end;

theorem E9: :: CALCUL_1:5
for b1 being Element of CQC-WFF
for b2 being FinSequence of CQC-WFF holds
( Suc (b2 ^ <*b1*>) = b1 & Ant (b2 ^ <*b1*>) = b2 )
proof
let c1 be Element of CQC-WFF ;
let c2 be FinSequence of CQC-WFF ;
set c3 = c2 ^ <*c1*>;
E10: len (c2 ^ <*c1*>) = (len c2) + 1 by FINSEQ_2:19;
then E11: 0 < len (c2 ^ <*c1*>) ;
thus Suc (c2 ^ <*c1*>) = c1
proof
(c2 ^ <*c1*>) . (len (c2 ^ <*c1*>)) = c1 by E10, FINSEQ_1:59;
hence Suc (c2 ^ <*c1*>) = c1 by E11, E2;
end;
thus Ant (c2 ^ <*c1*>) = c2
proof
set c4 = c2 ^ <*c1*>;
now
let c5 be set ;
assume c5 in c2 ;
then consider c6 being Nat such that
E12: ( c6 in dom c2 & c5 = [c6,(c2 . c6)] ) by FINSEQ_1:16;
E13: c6 in dom (c2 ^ <*c1*>) by E12, FINSEQ_2:18;
c2 . c6 = (c2 ^ <*c1*>) . c6 by E12, FINSEQ_1:def 7;
hence c5 in c2 ^ <*c1*> by E12, E13, FUNCT_1:8;
end;
then c2 c= c2 ^ <*c1*> by TARSKI:def 3;
then E12: c2 = (c2 ^ <*c1*>) | (dom c2) by GRFUNC_1:64;
c2 = (c2 ^ <*c1*>) | (Seg (len c2)) by E12, FINSEQ_1:def 3;
hence Ant (c2 ^ <*c1*>) = c2 by E10, E1;
end;
end;

theorem E10: :: CALCUL_1:6
for b1, b2 being FinSequence holds
( len b1 <= len (b1 ^ b2) & len b2 <= len (b1 ^ b2) & ( b1 <> {} implies ( 1 <= len b1 & len b2 < len (b2 ^ b1) ) ) )
proof
let c1, c2 be FinSequence;
len (c1 ^ c2) = (len c1) + (len c2) by FINSEQ_1:35;
hence ( len c1 <= len (c1 ^ c2) & len c2 <= len (c1 ^ c2) ) by NAT_1:37;
assume c1 <> {} ;
then len c1 <> 0 by FINSEQ_1:25;
then 0 < len c1 ;
then E11: 0 + 1 <= len c1 by NAT_1:38;
then (len c2) + 1 <= (len c1) + (len c2) by XREAL_1:8;
then (len c2) + 1 <= len (c2 ^ c1) by FINSEQ_1:35;
hence ( 1 <= len c1 & len c2 < len (c2 ^ c1) ) by E11, NAT_1:38;
end;

theorem E11: :: CALCUL_1:7
for b1, b2 being FinSequence of CQC-WFF holds Seq ((b1 ^ b2) | (dom b1)) = (b1 ^ b2) | (dom b1)
proof
let c1, c2 be FinSequence of CQC-WFF ;
(c1 ^ c2) | (dom c1) = c1 by FINSEQ_1:33;
hence Seq ((c1 ^ c2) | (dom c1)) = (c1 ^ c2) | (dom c1) by GRAPH_2:24;
end;

theorem E12: :: CALCUL_1:8
for b1, b2 being FinSequence of CQC-WFF holds b1 is_Subsequence_of b1 ^ b2
proof
let c1, c2 be FinSequence of CQC-WFF ;
set c3 = len c1;
take c4 = Seg (len c1); :: uses CALCUL_1:def 4
reconsider c5 = (c1 ^ c2) | c4 as FinSequence by FINSEQ_1:19;
E13: c4 = dom c1 by FINSEQ_1:def 3;
then c1 c= c5 by FINSEQ_1:33;
hence c1 c= Seq ((c1 ^ c2) | c4) by E13, E11;
end;

theorem E13: :: CALCUL_1:9
for b1, b2 being set
for b3 being FinSequence holds
1 < len ((b3 ^ <*b1*>) ^ <*b2*>)
proof
let c1, c2 be set ;
let c3 be FinSequence;
len ((c3 ^ <*c1*>) ^ <*c2*>) = (len (c3 ^ <*c1*>)) + (len <*c2*>) by FINSEQ_1:35;
then len ((c3 ^ <*c1*>) ^ <*c2*>) = (len (c3 ^ <*c1*>)) + 1 by FINSEQ_1:56;
then len ((c3 ^ <*c1*>) ^ <*c2*>) = ((len c3) + (len <*c1*>)) + 1 by FINSEQ_1:35;
then len ((c3 ^ <*c1*>) ^ <*c2*>) = ((len c3) + 1) + 1 by FINSEQ_1:56;
then len ((c3 ^ <*c1*>) ^ <*c2*>) = (len c3) + (1 + 1) ;
then 1 + 1 <= len ((c3 ^ <*c1*>) ^ <*c2*>) by NAT_1:29;
hence 1 < len ((c3 ^ <*c1*>) ^ <*c2*>) by NAT_1:38;
end;

theorem E14: :: CALCUL_1:10
for b1 being set
for b2 being FinSequence holds
( 1 <= len (b2 ^ <*b1*>) & len (b2 ^ <*b1*>) in dom (b2 ^ <*b1*>) )
proof
let c1 be set ;
let c2 be FinSequence;
len (c2 ^ <*c1*>) = (len c2) + 1 by FINSEQ_2:19;
then 1 <= len (c2 ^ <*c1*>) by NAT_1:29;
hence ( 1 <= len (c2 ^ <*c1*>) & len (c2 ^ <*c1*>) in dom (c2 ^ <*c1*>) ) by FINSEQ_3:27;
end;

theorem E15: :: CALCUL_1:11
for b1, b2 being Nat holds
( 0 < b1 implies len (Sgm ((Seg b2) \/ {(b2 + b1)})) = b2 + 1 )
proof
let c1, c2 be Nat;
assume E16: 0 < c1 ;
then not c2 + c1 in Seg c2 by FINSEQ_3:11;
then card ((Seg c2) \/ {(c2 + c1)}) = (card (Seg c2)) + 1 by CARD_2:54;
then E17: card ((Seg c2) \/ {(c2 + c1)}) = c2 + 1 by FINSEQ_1:78;
0 + 1 <= c1 by E16, NAT_1:38;
then ( 1 <= c1 & c1 <= c2 + c1 ) by NAT_1:29;
then 1 <= c1 + c2 by XREAL_1:2;
then c2 + c1 in Seg (c2 + c1) by FINSEQ_1:3;
then E18: {(c2 + c1)} c= Seg (c2 + c1) by ZFMISC_1:37;
Seg c2 c= Seg (c2 + c1) by FINSEQ_3:19;
then (Seg c2) \/ {(c2 + c1)} c= Seg (c2 + c1) by E18, XBOOLE_1:8;
hence len (Sgm ((Seg c2) \/ {(c2 + c1)})) = c2 + 1 by E17, FINSEQ_3:44;
end;

theorem E16: :: CALCUL_1:12
for b1, b2 being Nat holds
( 0 < b1 implies dom (Sgm ((Seg b2) \/ {(b2 + b1)})) = Seg (b2 + 1) )
proof
let c1, c2 be Nat;
assume 0 < c1 ;
then len (Sgm ((Seg c2) \/ {(c2 + c1)})) = c2 + 1 by E15;
hence dom (Sgm ((Seg c2) \/ {(c2 + c1)})) = Seg (c2 + 1) by FINSEQ_1:def 3;
end;

theorem E17: :: CALCUL_1:13
for b1, b2 being FinSequence of CQC-WFF holds
( 0 < len b1 implies b1 is_Subsequence_of ((Ant b1) ^ b2) ^ <*(Suc b1)*> )
proof
let c1, c2 be FinSequence of CQC-WFF ;
set c3 = len (Ant c1);
set c4 = len c2;
set c5 = (Seg (len (Ant c1))) \/ {((len (Ant c1)) + ((len c2) + 1))};
set c6 = ((Ant c1) ^ c2) ^ <*(Suc c1)*>;
reconsider c7 = (((Ant c1) ^ c2) ^ <*(Suc c1)*>) | ((Seg (len (Ant c1))) \/ {((len (Ant c1)) + ((len c2) + 1))}) as FinSubsequence ;
assume E18: 0 < len c1 ;
E19: now
let c8 be set ;
assume E20: c8 in c1 ;
consider c9, c10 being set such that
E21: c8 = [c9,c10] by E20, RELAT_1:def 1;
E22: ( c9 in dom c1 & c10 = c1 . c9 ) by E20, E21, FUNCT_1:8;
now
let c11 be set ;
assume E23: c11 in (Seg (len (Ant c1))) \/ {((len (Ant c1)) + ((len c2) + 1))} ;
reconsider c12 = c11 as Nat by E23;
E24: now
assume c12 in Seg (len (Ant c1)) ;
then E25: ( 1 <= c12 & c12 <= len (Ant c1) ) by FINSEQ_1:3;
((Ant c1) ^ c2) ^ <*(Suc c1)*> = (Ant c1) ^ (c2 ^ <*(Suc c1)*>) by FINSEQ_1:45;
then len (Ant c1) <= len (((Ant c1) ^ c2) ^ <*(Suc c1)*>) by E10;
then ( 1 <= c12 & c12 <= len (((Ant c1) ^ c2) ^ <*(Suc c1)*>) ) by E25, XREAL_1:2;
hence c12 in dom (((Ant c1) ^ c2) ^ <*(Suc c1)*>) by FINSEQ_3:27;
end;
now
assume c12 in {((len (Ant c1)) + ((len c2) + 1))} ;
then E25: c12 = ((len (Ant c1)) + (len c2)) + 1 by TARSKI:def 1;
len (((Ant c1) ^ c2) ^ <*(Suc c1)*>) = (len ((Ant c1) ^ c2)) + (len <*(Suc c1)*>) by FINSEQ_1:35;
then len (((Ant c1) ^ c2) ^ <*(Suc c1)*>) = ((len (Ant c1)) + (len c2)) + (len <*(Suc c1)*>) by FINSEQ_1:35;
then ( 1 <= c12 & c12 <= len (((Ant c1) ^ c2) ^ <*(Suc c1)*>) ) by E25, FINSEQ_1:56, NAT_1:29;
hence c12 in dom (((Ant c1) ^ c2) ^ <*(Suc c1)*>) by FINSEQ_3:27;
end;
hence c11 in dom (((Ant c1) ^ c2) ^ <*(Suc c1)*>) by E23, E24, XBOOLE_0:def 2;
end;
then E23: (Seg (len (Ant c1))) \/ {((len (Ant c1)) + ((len c2) + 1))} c= dom (((Ant c1) ^ c2) ^ <*(Suc c1)*>) by TARSKI:def 3;
dom c7 = (dom (((Ant c1) ^ c2) ^ <*(Suc c1)*>)) /\ ((Seg (len (Ant c1))) \/ {((len (Ant c1)) + ((len c2) + 1))}) by RELAT_1:90;
then E24: dom c7 = (Seg (len (Ant c1))) \/ {((len (Ant c1)) + ((len c2) + 1))} by E23, XBOOLE_1:28;
E25: dom (Sgm (dom c7)) = Seg ((len (Ant c1)) + 1) by E24, E16;
now
let c11 be Nat;
( c11 in dom c1 iff ( 1 <= c11 & c11 <= len c1 ) ) by FINSEQ_3:27;
then ( c11 in dom c1 iff ( 1 <= c11 & c11 <= (len (Ant c1)) + 1 ) ) by E18, E6;
hence ( c11 in dom c1 iff c11 in Seg ((len (Ant c1)) + 1) ) by FINSEQ_1:3;
end;
then for b1 being set holds
( b1 in dom c1 iff b1 in Seg ((len (Ant c1)) + 1) ) ;
then E26: dom (Sgm (dom c7)) = dom c1 by E25, TARSKI:2;
reconsider c11 = c9 as Nat by E22;
E27: 0 + 1 <= (len c2) + 1 by NAT_1:38;
(len c2) + 1 <= (len (Ant c1)) + ((len c2) + 1) by NAT_1:29;
then 1 <= (len (Ant c1)) + ((len c2) + 1) by E27, XREAL_1:2;
then (len (Ant c1)) + ((len c2) + 1) in Seg ((len (Ant c1)) + ((len c2) + 1)) by FINSEQ_1:3;
then E28: {((len (Ant c1)) + ((len c2) + 1))} c= Seg ((len (Ant c1)) + ((len c2) + 1)) by ZFMISC_1:37;
now
let c12, c13 be Nat;
assume E29: ( c12 in Seg (len (Ant c1)) & c13 in {((len (Ant c1)) + ((len c2) + 1))} ) ;
E30: c12 <= len (Ant c1) by E29, FINSEQ_1:3;
(len (Ant c1)) + 1 <= ((len (Ant c1)) + 1) + (len c2) by NAT_1:29;
then len (Ant c1) < (len (Ant c1)) + ((len c2) + 1) by NAT_1:38;
then len (Ant c1) < c13 by E29, TARSKI:def 1;
hence c12 < c13 by E30, XREAL_1:2;
end;
then E29: Sgm (dom c7) = (Sgm (Seg (len (Ant c1)))) ^ (Sgm {((len (Ant c1)) + ((len c2) + 1))}) by E24, E28, FINSEQ_3:48;
Sgm (dom c7) = (Sgm (Seg (len (Ant c1)))) ^ <*((len (Ant c1)) + ((len c2) + 1))*> by E29, FINSEQ_3:50;
then E30: Sgm (dom c7) = (idseq (len (Ant c1))) ^ <*((len (Ant c1)) + ((len c2) + 1))*> by FINSEQ_3:54;
E31: now
assume E32: c11 in Seg (len (Ant c1)) ;
then c11 in dom (idseq (len (Ant c1))) by FINSEQ_2:54;
then (Sgm (dom c7)) . c11 = (idseq (len (Ant c1))) . c11 by E30, FINSEQ_1:def 7;
then E33: (Sgm (dom c7)) . c11 = c11 by E32, FINSEQ_2:56;
E34: c11 in dom (Sgm (dom c7)) by E20, E21, E26, FUNCT_1:8;
Seq c7 = c7 * (Sgm (dom c7)) by FINSEQ_1:def 14;
then E35: (Seq c7) . c11 = c7 . c11 by E33, E34, FUNCT_1:23;
E36: ( ((Ant c1) ^ c2) ^ <*(Suc c1)*> = (Ant c1) ^ (c2 ^ <*(Suc c1)*>) & Seg (len (Ant c1)) c= (Seg (len (Ant c1))) \/ {(