let S, T be Semilattice; :: thesis: for f being Function of S,T st f is meet-preserving holds
for X being non empty finite Subset of S holds f preserves_inf_of X
let f be Function of S,T; :: thesis: ( f is meet-preserving implies for X being non empty finite Subset of S holds f preserves_inf_of X )
assume A1: f is meet-preserving ; :: thesis: for X being non empty finite Subset of S holds f preserves_inf_of X
let X be non empty finite Subset of S; :: thesis: f preserves_inf_of X
assume ex_inf_of X,S ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of f .: X,T & "/\" (f .: X),T = f . ("/\" X,S) )
A2: X is finite ;
defpred S₁[ set ] means ( $1 <> {} implies ( ex_inf_of $1,S & ex_inf_of f .: $1,T & inf (f .: $1) = f . ("/\" $1,S) ) );
A3: S₁[ {} ] ;

A4: now

let y, x be set ; :: thesis: ( y in X & x c= X & S₁[x] implies S₁[x \/ {y}] )
assume that
A5: y in X and
x c= X and
A6: S₁[x] ; :: thesis: S₁[x \/ {y}]
thus S₁[x \/ {y}] :: thesis: verum

proof

assume x \/ {y} <> {} ; :: thesis: ( ex_inf_of x \/ {y},S & ex_inf_of f .: (x \/ {y}),T & inf (f .: (x \/ {y})) = f . ("/\" (x \/ {y}),S) )
reconsider y9 = y as Element of S by A5;
set fy = f . y9;
A7: ex_inf_of {(f . y9)},T by YELLOW_0:38;
A8: inf {(f . y9)} = f . y9 by YELLOW_0:39;
A9: ex_inf_of {y9},S by YELLOW_0:38;
A10: inf {y9} = y by YELLOW_0:39;
thus ex_inf_of x \/ {y},S by A6, A9, YELLOW_2:4; :: thesis: ( ex_inf_of f .: (x \/ {y}),T & inf (f .: (x \/ {y})) = f . ("/\" (x \/ {y}),S) )
dom f = the carrier of S by FUNCT_2:def 1;
then A11: Im f,y = {(f . y9)} by FUNCT_1:117;
then A12: f .: (x \/ {y}) = (f .: x) \/ {(f . y9)} by RELAT_1:153;
hence ex_inf_of f .: (x \/ {y}),T by A6, A7, A11, YELLOW_2:4; :: thesis: inf (f .: (x \/ {y})) = f . ("/\" (x \/ {y}),S)

per cases ( x = {} or x <> {} ) ;

suppose x = {} ; :: thesis: inf (f .: (x \/ {y})) = f . ("/\" (x \/ {y}),S)

hence inf (f .: (x \/ {y})) = f . ("/\" (x \/ {y}),S) by A8, A11, YELLOW_0:39; :: thesis: verum

end;

suppose A13: x <> {} ; :: thesis: inf (f .: (x \/ {y})) = f . ("/\" (x \/ {y}),S)

hence "/\" (f .: (x \/ {y})),T = (f . ("/\" x,S)) "/\" (f . y9) by A6, A7, A8, A12, YELLOW_2:4
.= f . (("/\" x,S) "/\" y9) by A1, WAYBEL_6:1
.= f . ("/\" (x \/ {y}),S) by A6, A9, A10, A13, YELLOW_2:4 ;
:: thesis: verum

end;

end;

end;

end;

S₁[X] from FINSET_1:sch 2(A2, A3, A4);
hence ( ex_inf_of f .: X,T & "/\" (f .: X),T = f . ("/\" X,S) ) ; :: thesis: verum