set A = { x where x is Element of F_{1}() : P_{1}[x] } ;

consider z being Element of F_{1}() such that

A3: P_{1}[z]
by A1;

A4: z in { x where x is Element of F_{1}() : P_{1}[x] }
by A3;

_{1}() is SN
by A4, ThSN; :: thesis: verum

consider z being Element of F

A3: P

A4: z in { x where x is Element of F

now :: thesis: for x being Element of F_{1}() st x in { x where x is Element of F_{1}() : P_{1}[x] } holds

ex y being Element of F_{1}() st

( y in { x where x is Element of F_{1}() : P_{1}[x] } & x ==> y )

hence
not Fex y being Element of F

( y in { x where x is Element of F

let x be Element of F_{1}(); :: thesis: ( x in { x where x is Element of F_{1}() : P_{1}[x] } implies ex y being Element of F_{1}() st

( y in { x where x is Element of F_{1}() : P_{1}[x] } & x ==> y ) )

assume x in { x where x is Element of F_{1}() : P_{1}[x] }
; :: thesis: ex y being Element of F_{1}() st

( y in { x where x is Element of F_{1}() : P_{1}[x] } & x ==> y )

then ex a being Element of F_{1}() st

( x = a & P_{1}[a] )
;

then consider y being Element of F_{1}() such that

A6: ( P_{1}[y] & x ==> y )
by A2;

take y = y; :: thesis: ( y in { x where x is Element of F_{1}() : P_{1}[x] } & x ==> y )

thus y in { x where x is Element of F_{1}() : P_{1}[x] }
by A6; :: thesis: x ==> y

thus x ==> y by A6; :: thesis: verum

end;( y in { x where x is Element of F

assume x in { x where x is Element of F

( y in { x where x is Element of F

then ex a being Element of F

( x = a & P

then consider y being Element of F

A6: ( P

take y = y; :: thesis: ( y in { x where x is Element of F

thus y in { x where x is Element of F

thus x ==> y by A6; :: thesis: verum