let Al be QC-alphabet ; :: thesis:
let f, g be FinSequence of CQC-WFF Al; :: thesis:
set h = Rev g;
assume that
A1: 1 <= len g and
A2: |- f ^ g ; :: thesis:
A3: 1 <= len (Rev g) by A1, FINSEQ_5:def 3;
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 A1, FINSEQ_5:def 3;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len F implies ex f1, f2 being FinSequence of CQC-WFF Al ex n being Nat st
( $1 + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . $1)*> & |- f2 ) );
A9: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A10: S₁[k] ; :: thesis:
A11: len g <= len (f ^ g) by CALCUL_1:6;
assume that
A12: 1 <= k + 1 and
A13: k + 1 <= len F ; :: thesis:
A14: k + 1 <= len g by A5, A13, FINSEQ_5:def 3;
then consider n being Nat such that
A15: len (f ^ g) = (k + 1) + n by A11, NAT_1:10, XXREAL_0:2;
reconsider n = n as Element of NAT by ORDINAL1:def 12;

A16: now :: thesis:

k + 1 in dom F by A12, A13, FINSEQ_3:25;
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:
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 Nat st
( k + n = len (f ^ g) & f1k = (f ^ g) | (Seg n) & f2 = f1k ^ <*(F . k)*> & |- f2 ) by A10, A13, NAT_1:13;
consider f2k being FinSequence of CQC-WFF Al such that
A20: ex n being Nat st
( k + n = len (f ^ g) & f1k = (f ^ g) | (Seg n) & f2k = f1k ^ <*(F . k)*> & |- f2k ) by A19;
consider nk being 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 A15, A21, A17, FINSEQ_3:25;
then reconsider p = (f ^ g) . nk as Element of CQC-WFF Al by FINSEQ_2:11;
n + 1 = nk by A15, A21;
then A25: f2k = (f1 ^ <*((f ^ g) . nk)*>) ^ <*(F . k)*> by A22, A24, FINSEQ_5:10;
A26: k < len (Rev g) by A5, A13, NAT_1:13;
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 A7, A18;
k + 1 in dom (Rev g) by A5, A12, A13, FINSEQ_3:25;
then k + 1 in dom g by FINSEQ_5:57;
then A29: p1 = g . (((len g) - (k + 1)) + 1) by A27, FINSEQ_5:58
.= g . ((len g) - k) ;
k < len g by A26, FINSEQ_5:def 3;
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 A30, INT_1:7;
then i in dom g by A31, FINSEQ_3:25;
then p1 = (f ^ g) . ((len f) + i) by A29, FINSEQ_1:def 7
.= (f ^ g) . (((len f) + (len g)) - k)
.= (f ^ g) . ((len (f ^ g)) - k) by FINSEQ_1:22
.= p by A21 ;
then |- f1 ^ <*r*> by A23, A25, A28, Th27;
hence ex f1, f2 being FinSequence of CQC-WFF Al ex n being Nat st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 ) by A15; :: thesis:

end;

A32: k + 1 <= len (f ^ g) by A14, A11, XXREAL_0:2;

now :: thesis:

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 A1, FINSEQ_3:25;
assume A35: k = 0 ; :: thesis:
then A36: (f ^ g) . (n + 1) = (f ^ g) . ((len f) + (len g)) by A15, FINSEQ_1:22;
1 <= len (f ^ g) by A12, A32, XXREAL_0:2;
then len (f ^ g) in dom (f ^ g) by FINSEQ_3:25;
then (f ^ g) | (Seg (n + 1)) = f1 ^ <*((f ^ g) . (n + 1))*> by A15, A35, FINSEQ_5:10;
then f1 ^ <*(F . 1)*> = (f ^ g) | (Seg (len (f ^ g))) by A15, A35, A33, A34, A36, FINSEQ_1:def 7;
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:
take f2 = f2; :: thesis:
take n = n; :: thesis:
|- f2 by A2, A37, RELAT_1:69;
hence ex f1, f2 being FinSequence of CQC-WFF Al ex n being Nat st
( (k + 1) + n = len (f ^ g) & f1 = (f ^ g) | (Seg n) & f2 = f1 ^ <*(F . (k + 1))*> & |- f2 ) by A15, A35; :: thesis:

end;

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

end;

A38: S₁[ 0 ] ;
for k being Nat holds S₁[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 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 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 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 A41, FINSEQ_5:def 3;
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 A4, A42, FINSEQ_1:21; :: thesis: