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)*>
A2:
now let b be
set ;
:: thesis: ( b in f implies b in Seq f2 )assume A3:
b in f
;
:: thesis: b in Seq f2consider c,
d being
set such that A4:
b = [c,d]
by A3, RELAT_1:def 1;
A5:
(
c in dom f &
d = f . c )
by A3, A4, FUNCT_1:8;
then A10:
(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 A11:
dom f2 = (Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))}
by A10, XBOOLE_1:28;
then A12:
dom (Sgm (dom f2)) = Seg ((len (Ant f)) + 1)
by Th12;
then
for
b being
set holds
(
b in dom f iff
b in Seg ((len (Ant f)) + 1) )
;
then A13:
dom (Sgm (dom f2)) = dom f
by A12, TARSKI:2;
reconsider i =
c as
Element of
NAT by A5;
A14:
0 + 1
<= (len g) + 1
by NAT_1:13;
(len g) + 1
<= (len (Ant f)) + ((len g) + 1)
by NAT_1:11;
then
1
<= (len (Ant f)) + ((len g) + 1)
by A14, XXREAL_0:2;
then
(len (Ant f)) + ((len g) + 1) in Seg ((len (Ant f)) + ((len g) + 1))
by FINSEQ_1:3;
then A15:
{((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 A11, A15, FINSEQ_3:48;
then
Sgm (dom f2) = (Sgm (Seg (len (Ant f)))) ^ <*((len (Ant f)) + ((len g) + 1))*>
by FINSEQ_3:50;
then A18:
Sgm (dom f2) = (idseq (len (Ant f))) ^ <*((len (Ant f)) + ((len g) + 1))*>
by FINSEQ_3:54;
A19:
now assume A20:
i in Seg (len (Ant f))
;
:: thesis: (Seq f2) . i = f . ithen
i in dom (idseq (len (Ant f)))
by RELAT_1:71;
then
(Sgm (dom f2)) . i = (idseq (len (Ant f))) . i
by A18, FINSEQ_1:def 7;
then A21:
(Sgm (dom f2)) . i = i
by A20, FUNCT_1:35;
A22:
i in dom (Sgm (dom f2))
by A3, A4, A13, FUNCT_1:8;
Seq f2 = f2 * (Sgm (dom f2))
by FINSEQ_1:def 14;
then A23:
(Seq f2) . i = f2 . i
by A21, A22, FUNCT_1:23;
A24:
(
((Ant f) ^ g) ^ <*(Suc f)*> = (Ant f) ^ (g ^ <*(Suc f)*>) &
Seg (len (Ant f)) c= (Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))} )
by FINSEQ_1:45, XBOOLE_1:7;
A25:
Seg (len (Ant f)) = dom (Ant f)
by FINSEQ_1:def 3;
(Seq f2) . i = (f2 | (Seg (len (Ant f)))) . i
by A20, A23, FUNCT_1:72;
then
(Seq f2) . i = ((((Ant f) ^ g) ^ <*(Suc f)*>) | (Seg (len (Ant f)))) . i
by A24, RELAT_1:103;
then A26:
(Seq f2) . i = (Ant f) . i
by A24, A25, FINSEQ_1:33;
A27:
i in dom (Ant f)
by A20, FINSEQ_1:def 3;
f = (Ant f) ^ <*(Suc f)*>
by A1, Th3;
hence
(Seq f2) . i = f . i
by A26, A27, FINSEQ_1:def 7;
:: thesis: verum end; A28:
now assume A29:
i = (len (Ant f)) + 1
;
:: thesis: (Seq f2) . i = f . ithen
f . i = f . (len f)
by A1, Th2;
then A30:
f . i = Suc f
by A1, Def2;
len (idseq (len (Ant f))) = len (Ant f)
by FINSEQ_1:def 18;
then A31:
(Sgm (dom f2)) . i = (len (Ant f)) + ((len g) + 1)
by A18, A29, FINSEQ_1:59;
A32:
i in dom (Sgm (dom f2))
by A3, A4, A13, FUNCT_1:8;
Seq f2 = f2 * (Sgm (dom f2))
by FINSEQ_1:def 14;
then A33:
(Seq f2) . i = f2 . ((len (Ant f)) + ((len g) + 1))
by A31, A32, FUNCT_1:23;
A34:
(len (Ant f)) + ((len g) + 1) in {((len (Ant f)) + ((len g) + 1))}
by TARSKI:def 1;
{((len (Ant f)) + ((len g) + 1))} c= (Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))}
by XBOOLE_1:7;
then A35:
(Seq f2) . i = (((Ant f) ^ g) ^ <*(Suc f)*>) . (((len (Ant f)) + (len g)) + 1)
by A33, A34, FUNCT_1:72;
A36:
len ((Ant f) ^ g) = (len (Ant f)) + (len g)
by FINSEQ_1:35;
1
in Seg 1
by FINSEQ_1:3;
then
1
in dom <*(Suc f)*>
by FINSEQ_1:55;
then
(Seq f2) . i = <*(Suc f)*> . 1
by A35, A36, FINSEQ_1:def 7;
hence
(Seq f2) . i = f . i
by A30, FINSEQ_1:57;
:: 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 A13, RELAT_1:46;
then
dom f = dom (Seq f2)
by FINSEQ_1:def 14;
hence
b in Seq f2
by A4, A5, A12, A13, A19, A28, FINSEQ_2:8, FUNCT_1:8;
:: thesis: verum end;
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))}))
thus
f c= Seq ((((Ant f) ^ g) ^ <*(Suc f)*>) | ((Seg (len (Ant f))) \/ {((len (Ant f)) + ((len g) + 1))}))
by A2, TARSKI:def 3; :: thesis: verum