defpred S_{1}[ object , object ] means ex A being binary-image of E st

( $1 = A & $2 = A (-) B );

A2: for x being object st x in bool the carrier of E holds

S_{1}[x,f . x]
from FUNCT_2:sch 1(A1);

take f ; :: thesis: for A being binary-image of E holds f . A = A (-) B

( $1 = A & $2 = A (-) B );

A1: now :: thesis: for x being object st x in bool the carrier of E holds

ex y being object st

( y in bool the carrier of E & S_{1}[x,y] )

consider f being Function of (bool the carrier of E),(bool the carrier of E) such that ex y being object st

( y in bool the carrier of E & S

let x be object ; :: thesis: ( x in bool the carrier of E implies ex y being object st

( y in bool the carrier of E & S_{1}[x,y] ) )

assume x in bool the carrier of E ; :: thesis: ex y being object st

( y in bool the carrier of E & S_{1}[x,y] )

then reconsider A = x as binary-image of E ;

set y = A (-) B;

A (-) B c= the carrier of E ;

hence ex y being object st

( y in bool the carrier of E & S_{1}[x,y] )
; :: thesis: verum

end;( y in bool the carrier of E & S

assume x in bool the carrier of E ; :: thesis: ex y being object st

( y in bool the carrier of E & S

then reconsider A = x as binary-image of E ;

set y = A (-) B;

A (-) B c= the carrier of E ;

hence ex y being object st

( y in bool the carrier of E & S

A2: for x being object st x in bool the carrier of E holds

S

take f ; :: thesis: for A being binary-image of E holds f . A = A (-) B

now :: thesis: for A being binary-image of E holds f . A = A (-) B

hence
for A being binary-image of E holds f . A = A (-) B
; :: thesis: verumlet A be binary-image of E; :: thesis: f . A = A (-) B

ex X being binary-image of E st

( A = X & f . A = X (-) B ) by A2;

hence f . A = A (-) B ; :: thesis: verum

end;ex X being binary-image of E st

( A = X & f . A = X (-) B ) by A2;

hence f . A = A (-) B ; :: thesis: verum