let L1, L2, L3 be non empty reflexive antisymmetric RelStr ; :: thesis: for f being Function of L1,L2
for g being Function of L2,L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
g * f is filtered-infs-preserving
let f be Function of L1,L2; :: thesis: for g being Function of L2,L3 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
g * f is filtered-infs-preserving
let g be Function of L2,L3; :: thesis: ( f is filtered-infs-preserving & g is filtered-infs-preserving implies g * f is filtered-infs-preserving )
assume that
A1: f is filtered-infs-preserving and
A2: g is filtered-infs-preserving ; :: thesis: g * f is filtered-infs-preserving
set gf = g * f;
let X be Subset of L1; :: according to WAYBEL_0:def 36 :: thesis: ( X is empty or not X is filtered or g * f preserves_inf_of X )
assume that
A3: ( not X is empty & X is filtered ) and
A4: ex_inf_of X,L1 ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of (g * f) .: X,L3 & "/\" (((g * f) .: X),L3) = (g * f) . ("/\" (X,L1)) )
set xx = the Element of X;
set fX = f .: X;
set gfX = (g * f) .: X;
A5: f preserves_inf_of X by A1, A3;
then A6: ( (g * f) .: X = g .: (f .: X) & ex_inf_of f .: X,L2 ) by A4, RELAT_1:126;
the Element of X in X by A3;
then f . the Element of X in f .: X by FUNCT_2:35;
then ( not f .: X is empty & f .: X is filtered ) by A1, A3, Th23, Th24;
then A7: g preserves_inf_of f .: X by A2;
hence ex_inf_of (g * f) .: X,L3 by A6; :: thesis: "/\" (((g * f) .: X),L3) = (g * f) . ("/\" (X,L1))
A8: dom f = the carrier of L1 by FUNCT_2:def 1;
thus inf ((g * f) .: X) = g . (inf (f .: X)) by A7, A6
.= g . (f . (inf X)) by A4, A5
.= (g * f) . (inf X) by A8, FUNCT_1:13 ; :: thesis: verum