let H be Element of QC-WFF A; :: thesis: ex n being Nat ex L being FinSequence st
( 1 <= n & len L = n & L . 1 = H & L . n = H & ( for k being Nat st 1 <= k & k < n holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
reconsider L = <*H*> as FinSequence ;
take 1 ; :: thesis: ex L being FinSequence st
( 1 <= 1 & len L = 1 & L . 1 = H & L . 1 = H & ( for k being Nat st 1 <= k & k < 1 holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
take L ; :: thesis: ( 1 <= 1 & len L = 1 & L . 1 = H & L . 1 = H & ( for k being Nat st 1 <= k & k < 1 holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ) )
thus ( 1 <= 1 & len L = 1 & L . 1 = H & L . 1 = H ) by FINSEQ_1:40; :: thesis: for k being Nat st 1 <= k & k < 1 holds
ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
let k be Nat; :: thesis: ( 1 <= k & k < 1 implies ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) )
assume ( 1 <= k & k < 1 ) ; :: thesis: ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 )
hence ex G1, H1 being Element of QC-WFF A st
( L . k = G1 & L . (k + 1) = H1 & G1 is_immediate_constituent_of H1 ) ; :: thesis: verum