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 A5: ( y in X & x c= X & 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 y' = y as Element of S by A5;
set fy = f . y';
A6: ( ex_inf_of {(f . y')},T & inf {(f . y')} = f . y' & ex_inf_of {y'},S & inf {y'} = y ) by YELLOW_0:38, YELLOW_0:39;
hence ex_inf_of x \/ {y},S by A5, 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 A7: Im f,y = {(f . y')} by FUNCT_1:117;
then A8: f .: (x \/ {y}) = (f .: x) \/ {(f . y')} by RELAT_1:153;
hence ex_inf_of f .: (x \/ {y}),T by A5, A6, A7, 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 A6, A7; :: thesis: verum

end;

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

hence "/\" (f .: (x \/ {y})),T = (f . ("/\" x,S)) "/\" (f . y') by A5, A6, A8, YELLOW_2:4
.= f . (("/\" x,S) "/\" y') by A1, WAYBEL_6:1
.= f . ("/\" (x \/ {y}),S) by A5, A6, A9, 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