let L1, L2, T1, T2 be non empty reflexive antisymmetric RelStr ; :: thesis: for f being Function of L1,T1
for g being Function of L2,T2 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
[:f,g:] is filtered-infs-preserving
let f be Function of L1,T1; :: thesis: for g being Function of L2,T2 st f is filtered-infs-preserving & g is filtered-infs-preserving holds
[:f,g:] is filtered-infs-preserving
let g be Function of L2,T2; :: thesis: ( f is filtered-infs-preserving & g is filtered-infs-preserving implies [:f,g:] is filtered-infs-preserving )
assume A1: ( f is filtered-infs-preserving & g is filtered-infs-preserving ) ; :: thesis: [:f,g:] is filtered-infs-preserving
let X be Subset of [:L1,L2:]; :: according to WAYBEL_0:def 36 :: thesis: ( X is empty or not X is filtered or [:f,g:] preserves_inf_of X )
assume ( not X is empty & X is filtered ) ; :: thesis: [:f,g:] preserves_inf_of X
then ( not proj1 X is empty & proj1 X is filtered & not proj2 X is empty & proj2 X is filtered ) by YELLOW_3:21, YELLOW_3:24;
then A2: ( f preserves_inf_of proj1 X & g preserves_inf_of proj2 X ) by A1, WAYBEL_0:def 36;
assume A3: ex_inf_of X,[:L1,L2:] ; :: according to WAYBEL_0:def 30 :: thesis: ( ex_inf_of [:f,g:] .: X,[:T1,T2:] & "/\" ([:f,g:] .: X),[:T1,T2:] = [:f,g:] . ("/\" X,[:L1,L2:]) )
then A4: ( ex_inf_of proj1 X,L1 & ex_inf_of proj2 X,L2 ) by YELLOW_3:42;
set iX = [:f,g:] .: X;
A5: ( dom f = the carrier of L1 & dom g = the carrier of L2 ) by FUNCT_2:def 1;
X c= the carrier of [:L1,L2:] ;
then X c= [:the carrier of L1,the carrier of L2:] by YELLOW_3:def 2;
then A6: ( proj1 ([:f,g:] .: X) = f .: (proj1 X) & proj2 ([:f,g:] .: X) = g .: (proj2 X) ) by A5, Th4;
then ( ex_inf_of proj1 ([:f,g:] .: X),T1 & ex_inf_of proj2 ([:f,g:] .: X),T2 ) by A2, A4, WAYBEL_0:def 30;
hence ex_inf_of [:f,g:] .: X,[:T1,T2:] by YELLOW_3:42; :: thesis: "/\" ([:f,g:] .: X),[:T1,T2:] = [:f,g:] . ("/\" X,[:L1,L2:])
hence inf ([:f,g:] .: X) = [(inf (f .: (proj1 X))),(inf (g .: (proj2 X)))] by A6, Th7
.= [(f . (inf (proj1 X))),(inf (g .: (proj2 X)))] by A2, A4, WAYBEL_0:def 30
.= [(f . (inf (proj1 X))),(g . (inf (proj2 X)))] by A2, A4, WAYBEL_0:def 30
.= [:f,g:] . (inf (proj1 X)),(inf (proj2 X)) by A5, FUNCT_3:def 9
.= [:f,g:] . (inf X) by A3, Th7 ;
:: thesis: verum