let a be object ; :: thesis: ( F₁(),F₂() |- a implies P₁[a] )
assume F₁(),F₂() |- a ; :: thesis: P₁[a]
then consider P being Formula-sequence such that
A3: a in rng P and
A4: P is F₁(),F₂() -correct ;
defpred S₁[ Nat] means ( $1 in dom P implies P₁[P . $1] );
A10: for i being Nat st ( for j being Nat st j < i holds
S₁[j] ) holds
S₁[i]

proof

let i be Nat; :: thesis: ( ( for j being Nat st j < i holds
S₁[j] ) implies S₁[i] )
assume A11: for j being Nat st j < i holds
S₁[j] ; :: thesis: S₁[i]
reconsider k = i as Element of NAT by ORDINAL1:def 12;
assume i in dom P ; :: thesis: P₁[P . i]
then P,k is_a_correct_step_wrt F₁(),F₂() by A4;

per cases then ( P . i in F₁() or ex Q being Formula-finset st
( [Q,(P . i)] in F₂() & ( for t being Formula st t in Q holds
ex k being Nat st
( k in dom P & k < i & P . k = t ) ) ) ) ;

suppose P . i in F₁() ; :: thesis: P₁[P . i]

hence P₁[P . i] by A1; :: thesis: verum

end;

suppose ex Q being Formula-finset st
( [Q,(P . i)] in F₂() & ( for t being Formula st t in Q holds
ex k being Nat st
( k in dom P & k < i & P . k = t ) ) ) ; :: thesis: P₁[P . i]

then consider Q being Formula-finset such that
A14: [Q,(P . i)] in F₂() and
A15: for t being Formula st t in Q holds
ex k being Nat st
( k in dom P & k < i & P . k = t ) ;
for b being object st b in Q holds
P₁[b]

proof

let b be object ; :: thesis: ( b in Q implies P₁[b] )
assume b in Q ; :: thesis: P₁[b]
then consider k being Nat such that
A17: ( k in dom P & k < i & P . k = b ) by A15;
thus P₁[b] by A11, A17; :: thesis: verum

end;

hence P₁[P . i] by A2, A14; :: thesis: verum

end;

end;

end;

A30: for i being Nat holds S₁[i] from NAT_1:sch 4(A10);
consider b being object such that
A31: b in dom P and
A32: P . b = a by A3, FUNCT_1:def 3;
b in Seg (len P) by A31, FINSEQ_1:def 3;
hence P₁[a] by A30, A31, A32; :: thesis: verum