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 :: thesis: for y, x being set st y in X & x c= X & S₁[x] holds
S₁[x \/ {y}]

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:59;
then A12: f .: (x \/ {y}) = (f .: x) \/ {(f . y9)} by RELAT_1:120;
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