defpred S₁[ object , object ] means ( ( ex n being Nat st $1 in B . n & $1 in B . $2 ) or ( ( for n being Nat holds not $1 in B . n ) & $2 = 0 ) );
B1: for a being object st a in X holds
ex b being object st
( b in NAT & S₁[a,b] )

proof

let a be object ; :: thesis: ( a in X implies ex b being object st
( b in NAT & S₁[a,b] ) )
assume a in X ; :: thesis: ex b being object st
( b in NAT & S₁[a,b] )

per cases ( ex n being Nat st a in B . n or for n being Nat holds not a in B . n ) ;

suppose ex n being Nat st a in B . n ; :: thesis: ex b being object st
( b in NAT & S₁[a,b] )

then consider n being Nat such that
B3: a in B . n ;
take n ; :: thesis: ( n in NAT & S₁[a,n] )
thus ( n in NAT & S₁[a,n] ) by B3, ORDINAL1:def 12; :: thesis: verum

end;

suppose B10: for n being Nat holds not a in B . n ; :: thesis: ex b being object st
( b in NAT & S₁[a,b] )

take 0 ; :: thesis: ( 0 in NAT & S₁[a, 0 ] )
thus ( 0 in NAT & S₁[a, 0 ] ) by B10, ORDINAL1:def 12; :: thesis: verum

end;

end;

end;

consider f being Function of X,NAT such that
C2: for a being object st a in X holds
S₁[a,f . a] from FUNCT_2:sch 1(B1);
take f ; :: thesis: for a being object holds
( not a in X or ( ex n being Nat st a in B . n & a in B . (f . a) ) or ( ( for n being Nat holds not a in B . n ) & f . a = 0 ) )
thus for a being object holds
( not a in X or ( ex n being Nat st a in B . n & a in B . (f . a) ) or ( ( for n being Nat holds not a in B . n ) & f . a = 0 ) ) by C2; :: thesis: verum