defpred S1[ object , object ] means ex A being binary-image of E st
( \$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 & S1[x,y] )
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 & S1[x,y] ) )

assume x in bool the carrier of E ; :: thesis: ex y being object st
( y in bool the carrier of E & S1[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 & S1[x,y] ) ; :: thesis: verum
end;
consider f being Function of (bool the carrier of E),(bool the carrier of E) such that
A2: for x being object st x in bool the carrier of E holds
S1[x,f . x] from 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
let 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;
hence for A being binary-image of E holds f . A = A (-) B ; :: thesis: verum