let f, g be FinSequence of CQC-WFF ; :: thesis: ( 0 < len f implies f is_Subsequence_of ((Ant f) ^ g) ^ <*(Suc f)*> )
set n = len (Ant f);
set m = len g;
set N = (Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))};
set f1 = ((Ant f) ^ g) ^ <*(Suc f)*>;
reconsider f2 = (((Ant f) ^ g) ^ <*(Suc f)*>) | ((Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))}) as FinSubsequence ;
assume A1: 0 < len f ; :: thesis: f is_Subsequence_of ((Ant f) ^ g) ^ <*(Suc f)*>
take (Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))} ; :: according to CALCUL_1:def 4 :: thesis: f c= Seq ((((Ant f) ^ g) ^ <*(Suc f)*>) | ((Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))}))

now

now

let b be set ; :: thesis: ( b in (Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))} implies b in dom (((Ant f) ^ g) ^ <*(Suc f)*>) )
assume A2: b in (Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))} ; :: thesis: b in dom (((Ant f) ^ g) ^ <*(Suc f)*>)
reconsider i = b as Element of NAT by A2;

A3: now

assume i in {((len (Ant f)) + ((len g) + 1))} ; :: thesis: i in dom (((Ant f) ^ g) ^ <*(Suc f)*>)
then A4: i = ((len (Ant f)) + (len g)) + 1 by TARSKI:def 1;
then A5: 1 <= i by NAT_1:11;
len (((Ant f) ^ g) ^ <*(Suc f)*>) = (len ((Ant f) ^ g)) + (len <*(Suc f)*>) by FINSEQ_1:35;
then len (((Ant f) ^ g) ^ <*(Suc f)*>) = ((len (Ant f)) + (len g)) + (len <*(Suc f)*>) by FINSEQ_1:35;
then i <= len (((Ant f) ^ g) ^ <*(Suc f)*>) by A4, FINSEQ_1:56;
hence i in dom (((Ant f) ^ g) ^ <*(Suc f)*>) by A5, FINSEQ_3:27; :: thesis: verum

end;

now

((Ant f) ^ g) ^ <*(Suc f)*> = (Ant f) ^ (g ^ <*(Suc f)*>) by FINSEQ_1:45;
then A6: len (Ant f) <= len (((Ant f) ^ g) ^ <*(Suc f)*>) by Th6;
assume A7: i in Seg (len (Ant f)) ; :: thesis: i in dom (((Ant f) ^ g) ^ <*(Suc f)*>)
then A8: 1 <= i by FINSEQ_1:3;
i <= len (Ant f) by A7, FINSEQ_1:3;
then i <= len (((Ant f) ^ g) ^ <*(Suc f)*>) by A6, XXREAL_0:2;
hence i in dom (((Ant f) ^ g) ^ <*(Suc f)*>) by A8, FINSEQ_3:27; :: thesis: verum

end;

hence b in dom (((Ant f) ^ g) ^ <*(Suc f)*>) by A2, A3, XBOOLE_0:def 3; :: thesis: verum

end;

then A9: (Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))} c= dom (((Ant f) ^ g) ^ <*(Suc f)*>) by TARSKI:def 3;
dom f2 = (dom (((Ant f) ^ g) ^ <*(Suc f)*>)) /\ ((Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))}) by RELAT_1:90;
then A10: dom f2 = (Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))} by A9, XBOOLE_1:28;
then A11: dom (Sgm (dom f2)) = Seg ((len (Ant f)) + 1) by Th12;

now

let i be Element of NAT ; :: thesis: ( i in dom f iff i in Seg ((len (Ant f)) + 1) )
( i in dom f iff ( 1 <= i & i <= len f ) ) by FINSEQ_3:27;
then ( i in dom f iff ( 1 <= i & i <= (len (Ant f)) + 1 ) ) by A1, Th2;
hence ( i in dom f iff i in Seg ((len (Ant f)) + 1) ) by FINSEQ_1:3; :: thesis: verum

end;

then for b being set holds
( b in dom f iff b in Seg ((len (Ant f)) + 1) ) ;
then A12: dom (Sgm (dom f2)) = dom f by A11, TARSKI:2;

A13: now

let i, j be Element of NAT ; :: thesis: ( i in Seg (len (Ant f)) & j in {((len (Ant f)) + ((len g) + 1))} implies i < j )
assume that
A14: i in Seg (len (Ant f)) and
A15: j in {((len (Ant f)) + ((len g) + 1))} ; :: thesis: i < j
A16: i <= len (Ant f) by A14, FINSEQ_1:3;
(len (Ant f)) + 1 <= ((len (Ant f)) + 1) + (len g) by NAT_1:11;
then len (Ant f) < (len (Ant f)) + ((len g) + 1) by NAT_1:13;
then len (Ant f) < j by A15, TARSKI:def 1;
hence i < j by A16, XXREAL_0:2; :: thesis: verum

end;

let b be set ; :: thesis: ( b in f implies b in Seq f2 )
assume A17: b in f ; :: thesis: b in Seq f2
consider c, d being set such that
A18: b = [c,d] by A17, RELAT_1:def 1;
A19: c in dom f by A17, A18, FUNCT_1:8;
then reconsider i = c as Element of NAT ;
( 0 + 1 <= (len g) + 1 & (len g) + 1 <= (len (Ant f)) + ((len g) + 1) ) by NAT_1:11;
then 1 <= (len (Ant f)) + ((len g) + 1) by XXREAL_0:2;
then (len (Ant f)) + ((len g) + 1) in Seg ((len (Ant f)) + ((len g) + 1)) by FINSEQ_1:3;
then {((len (Ant f)) + ((len g) + 1))} c= Seg ((len (Ant f)) + ((len g) + 1)) by ZFMISC_1:37;
then Sgm (dom f2) = (Sgm (Seg (len (Ant f)))) ^ (Sgm {((len (Ant f)) + ((len g) + 1))}) by A10, A13, FINSEQ_3:48;
then Sgm (dom f2) = (Sgm (Seg (len (Ant f)))) ^ <*((len (Ant f)) + ((len g) + 1))*> by FINSEQ_3:50;
then A20: Sgm (dom f2) = (idseq (len (Ant f))) ^ <*((len (Ant f)) + ((len g) + 1))*> by FINSEQ_3:54;

A21: now

assume A22: i in Seg (len (Ant f)) ; :: thesis: (Seq f2) . i = f . i
then A23: i in dom (Ant f) by FINSEQ_1:def 3;
i in dom (idseq (len (Ant f))) by A22, RELAT_1:71;
then (Sgm (dom f2)) . i = (idseq (len (Ant f))) . i by A20, FINSEQ_1:def 7;
then A24: (Sgm (dom f2)) . i = i by A22, FUNCT_1:35;
( i in dom (Sgm (dom f2)) & Seq f2 = f2 * (Sgm (dom f2)) ) by A17, A18, A12, FINSEQ_1:def 14, FUNCT_1:8;
then (Seq f2) . i = f2 . i by A24, FUNCT_1:23;
then (Seq f2) . i = (f2 | (Seg (len (Ant f)))) . i by A22, FUNCT_1:72;
then A25: (Seq f2) . i = ((((Ant f) ^ g) ^ <*(Suc f)*>) | (Seg (len (Ant f)))) . i by RELAT_1:103, XBOOLE_1:7;
( ((Ant f) ^ g) ^ <*(Suc f)*> = (Ant f) ^ (g ^ <*(Suc f)*>) & Seg (len (Ant f)) = dom (Ant f) ) by FINSEQ_1:45, FINSEQ_1:def 3;
then A26: (Seq f2) . i = (Ant f) . i by A25, FINSEQ_1:33;
f = (Ant f) ^ <*(Suc f)*> by A1, Th3;
hence (Seq f2) . i = f . i by A26, A23, FINSEQ_1:def 7; :: thesis: verum

end;

rng (Sgm (dom ((((Ant f) ^ g) ^ <*(Suc f)*>) | ((Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))})))) = dom ((((Ant f) ^ g) ^ <*(Suc f)*>) | ((Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))})) by FINSEQ_1:71;
then dom f = dom (((((Ant f) ^ g) ^ <*(Suc f)*>) | ((Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))})) * (Sgm (dom ((((Ant f) ^ g) ^ <*(Suc f)*>) | ((Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))}))))) by A12, RELAT_1:46;
then A27: dom f = dom (Seq f2) by FINSEQ_1:def 14;

A28: now

1 in Seg 1 by FINSEQ_1:3;
then A29: ( len ((Ant f) ^ g) = (len (Ant f)) + (len g) & 1 in dom <*(Suc f)*> ) by FINSEQ_1:35, FINSEQ_1:55;
A30: ( i in dom (Sgm (dom f2)) & Seq f2 = f2 * (Sgm (dom f2)) ) by A17, A18, A12, FINSEQ_1:def 14, FUNCT_1:8;
assume A31: i = (len (Ant f)) + 1 ; :: thesis: (Seq f2) . i = f . i
len (idseq (len (Ant f))) = len (Ant f) by FINSEQ_1:def 18;
then (Sgm (dom f2)) . i = (len (Ant f)) + ((len g) + 1) by A20, A31, FINSEQ_1:59;
then A32: (Seq f2) . i = f2 . ((len (Ant f)) + ((len g) + 1)) by A30, FUNCT_1:23;
( (len (Ant f)) + ((len g) + 1) in {((len (Ant f)) + ((len g) + 1))} & {((len (Ant f)) + ((len g) + 1))} c= (Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))} ) by TARSKI:def 1, XBOOLE_1:7;
then (Seq f2) . i = (((Ant f) ^ g) ^ <*(Suc f)*>) . (((len (Ant f)) + (len g)) + 1) by A32, FUNCT_1:72;
then A33: (Seq f2) . i = <*(Suc f)*> . 1 by A29, FINSEQ_1:def 7;
f . i = f . (len f) by A1, A31, Th2;
then f . i = Suc f by A1, Def2;
hence (Seq f2) . i = f . i by A33, FINSEQ_1:57; :: thesis: verum

end;

d = f . c by A17, A18, FUNCT_1:8;
hence b in Seq f2 by A18, A19, A11, A12, A21, A28, A27, FINSEQ_2:8, FUNCT_1:8; :: thesis: verum

end;

hence f c= Seq ((((Ant f) ^ g) ^ <*(Suc f)*>) | ((Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))})) by TARSKI:def 3; :: thesis: verum