ex n being Element of NAT ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) by A1, QC_LANG2:def 20;
then consider L being FinSequence such that
A2: ex n being Element of NAT st
( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Element of NAT st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) ;
take L ; :: thesis: ( 1 <= len L & L . 1 = G & L . (len L) = H & ( for k being Element of NAT st 1 <= k & k < len L holds
ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus ( 1 <= len L & L . 1 = G & L . (len L) = H & ( for k being Element of NAT st 1 <= k & k < len L holds
ex G1, H1 being Element of QC-WFF st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) by A2; :: thesis: verum