let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al st 0 < len f holds
f is_Subsequence_of ((Ant f) ^ g) ^ <*(Suc f)*>
let f, g be FinSequence of CQC-WFF Al; :: 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 :: thesis: for b being object st b in f holds
b in Seq f2
now :: thesis: for b being object st b in (Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))} holds
b in dom (((Ant f) ^ g) ^ <*(Suc f)*>)
let b be object ; :: 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 :: thesis: ( i in {((len (Ant f)) + ((len g) + 1))} implies i in dom (((Ant f) ^ g) ^ <*(Suc f)*>) )
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:22;
then len (((Ant f) ^ g) ^ <*(Suc f)*>) = ((len (Ant f)) + (len g)) + (len <*(Suc f)*>) by FINSEQ_1:22;
then i <= len (((Ant f) ^ g) ^ <*(Suc f)*>) by A4, FINSEQ_1:39;
hence i in dom (((Ant f) ^ g) ^ <*(Suc f)*>) by A5, FINSEQ_3:25; :: thesis: verum
end;
now :: thesis: ( i in Seg (len (Ant f)) implies i in dom (((Ant f) ^ g) ^ <*(Suc f)*>) )
((Ant f) ^ g) ^ <*(Suc f)*> = (Ant f) ^ (g ^ <*(Suc f)*>) by FINSEQ_1:32;
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:1;
i <= len (Ant f) by A7, FINSEQ_1:1;
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:25; :: 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)*>) ;
dom f2 = (dom (((Ant f) ^ g) ^ <*(Suc f)*>)) /\ ((Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))}) by RELAT_1:61;
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 :: thesis: for i being Nat holds
( i in dom f iff i in Seg ((len (Ant f)) + 1) )
let i be 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:25;
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:1; :: thesis: verum
end;
then for b being object 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 :: thesis: for i, j being Nat st i in Seg (len (Ant f)) & j in {((len (Ant f)) + ((len g) + 1))} holds
i < j
let i, j be 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:1;
(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 object ; :: thesis: ( b in f implies b in Seq f2 )
assume A17: b in f ; :: thesis: b in Seq f2
consider c, d being object such that
A18: b = [c,d] by A17, RELAT_1:def 1;
A19: c in dom f by A17, A18, FUNCT_1:1;
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:1;
then {((len (Ant f)) + ((len g) + 1))} c= Seg ((len (Ant f)) + ((len g) + 1)) by ZFMISC_1:31;
then Sgm (dom f2) = (Sgm (Seg (len (Ant f)))) ^ (Sgm {((len (Ant f)) + ((len g) + 1))}) by A10, A13, FINSEQ_3:42;
then Sgm (dom f2) = (Sgm (Seg (len (Ant f)))) ^ <*((len (Ant f)) + ((len g) + 1))*> by FINSEQ_3:44;
then A20: Sgm (dom f2) = (idseq (len (Ant f))) ^ <*((len (Ant f)) + ((len g) + 1))*> by FINSEQ_3:48;
A21: now :: thesis: ( i in Seg (len (Ant f)) implies (Seq f2) . i = f . i )
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;
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:18;
( i in dom (Sgm (dom f2)) & Seq f2 = f2 * (Sgm (dom f2)) ) by A17, A18, A12, FINSEQ_1:def 14, FUNCT_1:1;
then (Seq f2) . i = f2 . i by A24, FUNCT_1:13;
then (Seq f2) . i = (f2 | (Seg (len (Ant f)))) . i by A22, FUNCT_1:49;
then A25: (Seq f2) . i = ((((Ant f) ^ g) ^ <*(Suc f)*>) | (Seg (len (Ant f)))) . i by RELAT_1:74, XBOOLE_1:7;
( ((Ant f) ^ g) ^ <*(Suc f)*> = (Ant f) ^ (g ^ <*(Suc f)*>) & Seg (len (Ant f)) = dom (Ant f) ) by FINSEQ_1:32, FINSEQ_1:def 3;
then A26: (Seq f2) . i = (Ant f) . i by A25, FINSEQ_1:21;
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:50;
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:27;
then A27: dom f = dom (Seq f2) by FINSEQ_1:def 14;
A28: now :: thesis: ( i = (len (Ant f)) + 1 implies (Seq f2) . i = f . i )
1 in Seg 1 by FINSEQ_1:1;
then A29: ( len ((Ant f) ^ g) = (len (Ant f)) + (len g) & 1 in dom <*(Suc f)*> ) by FINSEQ_1:22, FINSEQ_1:38;
A30: ( i in dom (Sgm (dom f2)) & Seq f2 = f2 * (Sgm (dom f2)) ) by A17, A18, A12, FINSEQ_1:def 14, FUNCT_1:1;
assume A31: i = (len (Ant f)) + 1 ; :: thesis: (Seq f2) . i = f . i
len (idseq (len (Ant f))) = len (Ant f) by CARD_1:def 7;
then (Sgm (dom f2)) . i = (len (Ant f)) + ((len g) + 1) by A20, A31, FINSEQ_1:42;
then A32: (Seq f2) . i = f2 . ((len (Ant f)) + ((len g) + 1)) by A30, FUNCT_1:13;
( (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:49;
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:40; :: thesis: verum
end;
d = f . c by A17, A18, FUNCT_1:1;
hence b in Seq f2 by A18, A19, A11, A12, A21, A28, A27, FINSEQ_2:7, FUNCT_1:1; :: thesis: verum
end;
hence f c= Seq ((((Ant f) ^ g) ^ <*(Suc f)*>) | ((Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))})) ; :: thesis: verum