ex n being Nat ex L being FinSequence st

( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Nat st 1 <= k & k < n holds

ex G1, H1 being Element of QC-WFF Al 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 Nat st

( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Nat st 1 <= k & k < n holds

ex G1, H1 being Element of QC-WFF Al 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 Nat st 1 <= k & k < len L holds

ex G1, H1 being Element of QC-WFF Al 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 Nat st 1 <= k & k < len L holds

ex G1, H1 being Element of QC-WFF Al st

( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) by A2; :: thesis: verum

( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Nat st 1 <= k & k < n holds

ex G1, H1 being Element of QC-WFF Al 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 Nat st

( 1 <= n & len L = n & L . 1 = G & L . n = H & ( for k being Nat st 1 <= k & k < n holds

ex G1, H1 being Element of QC-WFF Al 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 Nat st 1 <= k & k < len L holds

ex G1, H1 being Element of QC-WFF Al 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 Nat st 1 <= k & k < len L holds

ex G1, H1 being Element of QC-WFF Al st

( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) ) by A2; :: thesis: verum