reconsider Z = X null (AllFormulasOf S) as Element of bool (X \/ (AllFormulasOf S)) ;
deffunc H₁( Nat, Element of bool (X \/ (AllFormulasOf S))) -> Element of bool (X \/ (AllFormulasOf S)) = (X \/ (AllFormulasOf S)) typed/\ ((D,(num . $1)) AddFormulaTo $2);
consider f being sequence of (bool (X \/ (AllFormulasOf S))) such that
A1: ( f . 0 = Z & ( for n being Nat holds f . (n + 1) = H₁(n,f . n) ) ) from NAT_1:sch 12();
take f ; :: thesis: ( f . 0 = X & ( for m being Nat holds f . (m + 1) = (D,(num . m)) AddFormulaTo (f . m) ) )

now :: thesis: for n being Nat holds f . (n + 1) = (D,(num . n)) AddFormulaTo (f . n)

let n be Nat; :: thesis: f . (n + 1) = (D,(num . n)) AddFormulaTo (f . n)
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A2: ( (D,(num . nn)) AddFormulaTo (f . nn) c= (AllFormulasOf S) \/ (f . nn) & (AllFormulasOf S) \/ (f . nn) c= (AllFormulasOf S) \/ (X \/ (AllFormulasOf S)) ) by XBOOLE_1:9;
(AllFormulasOf S) \/ (X \/ (AllFormulasOf S)) = ((AllFormulasOf S) \/ (AllFormulasOf S)) \/ X by XBOOLE_1:4
.= X \/ (AllFormulasOf S) ;
then reconsider A = (D,(num . nn)) AddFormulaTo (f . nn) as Subset of (X \/ (AllFormulasOf S)) by XBOOLE_1:1, A2;
f . (n + 1) = A null (X \/ (AllFormulasOf S)) by A1;
hence f . (n + 1) = (D,(num . n)) AddFormulaTo (f . n) ; :: thesis: verum

end;

hence ( f . 0 = X & ( for m being Nat holds f . (m + 1) = (D,(num . m)) AddFormulaTo (f . m) ) ) by A1; :: thesis: verum