let S, T be sup-Semilattice; :: thesis: for f being Function of S,T holds
( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) )
let f be Function of S,T; :: thesis: ( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) )
A1: dom f = the carrier of S by FUNCT_2:def 1;
thus ( f is join-preserving implies for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) :: thesis: ( ( for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) implies f is join-preserving )

proof

assume A2: f is join-preserving ; :: thesis: for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y)
let z, y be Element of S; :: thesis: f . (z "\/" y) = (f . z) "\/" (f . y)
A3: f .: {z,y} = {(f . z),(f . y)} by A1, FUNCT_1:118;
A4: ex_sup_of {z,y},S by YELLOW_0:20;
A5: f preserves_sup_of {z,y} by A2, WAYBEL_0:def 35;
thus f . (z "\/" y) = f . (sup {z,y}) by YELLOW_0:41
.= sup {(f . z),(f . y)} by A3, A4, A5, WAYBEL_0:def 31
.= (f . z) "\/" (f . y) by YELLOW_0:41 ; :: thesis: verum

end;

assume A6: for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ; :: thesis: f is join-preserving
for z, y being Element of S holds f preserves_sup_of {z,y}

proof

let z, y be Element of S; :: thesis: f preserves_sup_of {z,y}
A7: f .: {z,y} = {(f . z),(f . y)} by A1, FUNCT_1:118;
then A8: ( ex_sup_of {z,y},S implies ex_sup_of f .: {z,y},T ) by YELLOW_0:20;
sup (f .: {z,y}) = (f . z) "\/" (f . y) by A7, YELLOW_0:41
.= f . (z "\/" y) by A6
.= f . (sup {z,y}) by YELLOW_0:41 ;
hence f preserves_sup_of {z,y} by A8, WAYBEL_0:def 31; :: thesis: verum

end;

hence f is join-preserving by WAYBEL_0:def 35; :: thesis: verum