let F, H be Element of QC-WFF ; :: thesis:
let x be bound_QC-variable; :: thesis:
H is_immediate_constituent_of All x,H by Th63;
hence ( F is_subformula_of H implies F is_proper_subformula_of All x,H ) by Th83; :: thesis:
given n being Element of NAT , L being FinSequence such that A1: ( 1 <= n & len L = n & L . 1 = F & L . n = All x,H ) and
A2: for k being Element of NAT st 1 <= k & k < n holds
ex H1, F1 being Element of QC-WFF st
( L . k = H1 & L . (k + 1) = F1 & H1 is_immediate_constituent_of F1 ) ; :: according to QC_LANG2:def 21,QC_LANG2:def 22 :: thesis:
assume F <> All x,H ; :: thesis:
then 1 < n by A1, XXREAL_0:1;
then 1 + 1 <= n by NAT_1:13;
then consider k being Nat such that
A3: n = 2 + k by NAT_1:10;
reconsider k = k as Element of NAT by ORDINAL1:def 13;
reconsider L1 = L | (Seg (1 + k)) as FinSequence by FINSEQ_1:19;
take m = 1 + k; :: according to QC_LANG2:def 21 :: thesis:
take L1 ; :: thesis:
thus A4: 1 <= m by NAT_1:11; :: thesis:
1 + k <= (1 + k) + 1 by NAT_1:11;
hence len L1 = m by A1, A3, FINSEQ_1:21; :: thesis:

A5: now

let j be Element of NAT ; :: thesis:
assume ( 1 <= j & j <= m ) ; :: thesis:
then j in Seg (1 + k) by FINSEQ_1:3;
hence L1 . j = L . j by FUNCT_1:72; :: thesis:

end;

hence L1 . 1 = F by A1, A4; :: thesis:
m < m + 1 by NAT_1:13;
then consider F1, G1 being Element of QC-WFF such that
A6: ( L . m = F1 & L . (m + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A2, A3, A4;
F1 = H by A1, A3, A6, Th63;
hence L1 . m = H by A4, A5, A6; :: thesis:
let j be Element of NAT ; :: thesis:
assume A7: ( 1 <= j & j < m ) ; :: thesis:
then A8: ( 1 <= 1 + j & 1 + j = j + 1 & j <= m & j + 1 <= m ) by NAT_1:13;
m <= m + 1 by NAT_1:11;
then j < n by A3, A7, XXREAL_0:2;
then consider F1, G1 being Element of QC-WFF such that
A9: ( L . j = F1 & L . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A2, A7;
take F1 ; :: thesis:
take G1 ; :: thesis:
thus ( L1 . j = F1 & L1 . (j + 1) = G1 & F1 is_immediate_constituent_of G1 ) by A5, A7, A8, A9; :: thesis: