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 preserves_sup_of {z,y} by A2;
A4: ( f .: {z,y} = {(f . z),(f . y)} & ex_sup_of {z,y},S ) by A1, FUNCT_1:60, YELLOW_0:20;
thus f . (z "\/" y) = f . (sup {z,y}) by YELLOW_0:41
.= sup {(f . z),(f . y)} by A4, A3
.= (f . z) "\/" (f . y) by YELLOW_0:41 ; :: thesis: verum

end;

assume A5: 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}
A6: f .: {z,y} = {(f . z),(f . y)} by A1, FUNCT_1:60;
then A7: ( 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 A6, YELLOW_0:41
.= f . (z "\/" y) by A5
.= f . (sup {z,y}) by YELLOW_0:41 ;
hence f preserves_sup_of {z,y} by A7; :: thesis: verum

end;

hence f is join-preserving ; :: thesis: verum