let Al be QC-alphabet ; :: thesis: for f, g being FinSequence of CQC-WFF Al st 1 <= len g & |- f ^ g holds
|- f ^ <*(Impl (Rev g))*>

let f, g be FinSequence of CQC-WFF Al; :: thesis: ( 1 <= len g & |- f ^ g implies |- f ^ <*(Impl (Rev g))*> )
set h = Rev g;
assume that
A1: 1 <= len g and
A2: |- f ^ g ; :: thesis: |- f ^ <*(Impl (Rev g))*>
A3: 1 <= len (Rev g) by ;
then consider F being FinSequence of CQC-WFF Al such that
A4: Impl (Rev g) = F . (len (Rev g)) and
A5: len F = len (Rev g) and
A6: ( F . 1 = Begin (Rev g) or len (Rev g) = 0 ) and
A7: for n being Nat st 1 <= n & n < len (Rev g) holds
ex p, q being Element of CQC-WFF Al st
( p = (Rev g) . (n + 1) & q = F . n & F . (n + 1) = p => q ) by Def4;
A8: 1 <= len (Rev g) by ;
defpred S1[ Nat] means ( 1 <= \$1 & \$1 <= len F implies ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( \$1 + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . \$1)*> & |- f2 ) );
A9: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A10: S1[k] ; :: thesis: S1[k + 1]
A11: len g <= len (f ^ g) by CALCUL_1:6;
assume that
A12: 1 <= k + 1 and
A13: k + 1 <= len F ; :: thesis: ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 )

A14: k + 1 <= len g by ;
then consider n being Nat such that
A15: len (f ^ g) = (k + 1) + n by ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
A16: now :: thesis: ( k <> 0 implies ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 ) )
k + 1 in dom F by ;
then reconsider r = F . (k + 1) as Element of CQC-WFF Al by FINSEQ_2:11;
set f1 = (f ^ g) | (Seg n);
reconsider f1 = (f ^ g) | (Seg n) as FinSequence of CQC-WFF Al by FINSEQ_1:18;
set f2 = f1 ^ <*r*>;
len (f ^ g) <= (len (f ^ g)) + k by NAT_1:11;
then A17: (len (f ^ g)) - k <= ((len (f ^ g)) + k) - k by XREAL_1:9;
assume k <> 0 ; :: thesis: ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 )

then A18: 0 + 1 <= k by NAT_1:13;
then consider f1k being FinSequence of CQC-WFF Al such that
A19: ex f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( k + n = len (f ^ g) & f1k = (f ^ g) | (Seg n) & f2 = f1k ^ <*(F . k)*> & |- f2 ) by ;
consider f2k being FinSequence of CQC-WFF Al such that
A20: ex n being Element of NAT st
( k + n = len (f ^ g) & f1k = (f ^ g) | (Seg n) & f2k = f1k ^ <*(F . k)*> & |- f2k ) by A19;
consider nk being Element of NAT such that
A21: k + nk = len (f ^ g) and
A22: ( f1k = (f ^ g) | (Seg nk) & f2k = f1k ^ <*(F . k)*> ) and
A23: |- f2k by A20;
1 <= n + 1 by NAT_1:11;
then A24: nk in dom (f ^ g) by ;
then reconsider p = (f ^ g) . nk as Element of CQC-WFF Al by FINSEQ_2:11;
n + 1 = nk by ;
then A25: f2k = (f1 ^ <*((f ^ g) . nk)*>) ^ <*(F . k)*> by ;
A26: k < len (Rev g) by ;
then consider p1, q1 being Element of CQC-WFF Al such that
A27: p1 = (Rev g) . (k + 1) and
A28: ( q1 = F . k & F . (k + 1) = p1 => q1 ) by ;
k + 1 in dom (Rev g) by ;
then k + 1 in dom g by FINSEQ_5:57;
then A29: p1 = g . (((len g) - (k + 1)) + 1) by
.= g . ((len g) - k) ;
k < len g by ;
then A30: k + (- k) < (len g) + (- k) by XREAL_1:8;
then reconsider i = (len g) - k as Element of NAT by INT_1:3;
len g <= k + (len g) by NAT_1:11;
then A31: i <= len g by XREAL_1:20;
0 + 1 <= i by ;
then i in dom g by ;
then p1 = (f ^ g) . ((len f) + i) by
.= (f ^ g) . (((len f) + (len g)) - k)
.= (f ^ g) . ((len (f ^ g)) - k) by FINSEQ_1:22
.= p by A21 ;
then |- f1 ^ <*r*> by ;
hence ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 ) by A15; :: thesis: verum
end;
A32: k + 1 <= len (f ^ g) by ;
now :: thesis: ( k = 0 implies ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 ) )
F . 1 = (Rev g) . 1 by A3, A6, Def3;
then A33: F . 1 = g . (len g) by FINSEQ_5:62;
set f1 = (f ^ g) | (Seg n);
reconsider f1 = (f ^ g) | (Seg n) as FinSequence of CQC-WFF Al by FINSEQ_1:18;
set f2 = f1 ^ <*(F . 1)*>;
A34: len g in dom g by ;
assume A35: k = 0 ; :: thesis: ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 )

then A36: (f ^ g) . (n + 1) = (f ^ g) . ((len f) + (len g)) by ;
1 <= len (f ^ g) by ;
then len (f ^ g) in dom (f ^ g) by FINSEQ_3:25;
then (f ^ g) | (Seg (n + 1)) = f1 ^ <*((f ^ g) . (n + 1))*> by ;
then f1 ^ <*(F . 1)*> = (f ^ g) | (Seg (len (f ^ g))) by ;
then A37: f1 ^ <*(F . 1)*> = (f ^ g) | (dom (f ^ g)) by FINSEQ_1:def 3;
then reconsider f2 = f1 ^ <*(F . 1)*> as FinSequence of CQC-WFF Al by RELAT_1:69;
take f1 = f1; :: thesis: ex f2 being FinSequence of CQC-WFF Al ex n being Element of NAT ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 )

take f2 = f2; :: thesis: ex n being Element of NAT ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 )

take n = n; :: thesis: ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 )

|- f2 by ;
hence ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 ) by ; :: thesis: verum
end;
hence ex f1, f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 ) by A16; :: thesis: verum
end;
A38: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch 2(A38, A9);
then consider f1 being FinSequence of CQC-WFF Al such that
A39: ex f2 being FinSequence of CQC-WFF Al ex n being Element of NAT st
( (len (Rev g)) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (len (Rev g)))*> & |- f2 ) by A5, A8;
consider f2 being FinSequence of CQC-WFF Al such that
A40: ex n being Element of NAT st
( (len (Rev g)) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (len (Rev g)))*> & |- f2 ) by A39;
consider n being Element of NAT such that
A41: (len (Rev g)) + n = len (f ^ g) and
A42: ( f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (len (Rev g)))*> & |- f2 ) by A40;
(n + (len (Rev g))) - (len (Rev g)) = (len (f ^ g)) - (len g) by ;
then (n + (len (Rev g))) + (- (len (Rev g))) = ((len f) + (len g)) - (len g) by FINSEQ_1:22;
then Seg n = dom f by FINSEQ_1:def 3;
hence |- f ^ <*(Impl (Rev g))*> by ; :: thesis: verum