let L1, L2, T1, T2 be non empty reflexive antisymmetric RelStr ; 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; 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; ( f is filtered-infs-preserving & g is filtered-infs-preserving implies [:f,g:] is filtered-infs-preserving )
assume that
A1:
f is filtered-infs-preserving
and
A2:
g is filtered-infs-preserving
; [:f,g:] is filtered-infs-preserving
let X be Subset of [:L1,L2:]; WAYBEL_0:def 36 ( X is empty or not X is filtered or [:f,g:] preserves_inf_of X )
assume A3:
( not X is empty & X is filtered )
; [:f,g:] preserves_inf_of X
then
( not proj1 X is empty & proj1 X is filtered )
by YELLOW_3:21, YELLOW_3:24;
then A4:
f preserves_inf_of proj1 X
by A1;
( not proj2 X is empty & proj2 X is filtered )
by A3, YELLOW_3:21, YELLOW_3:24;
then A5:
g preserves_inf_of proj2 X
by A2;
set iX = [:f,g:] .: X;
A6:
( dom f = the carrier of L1 & dom g = the carrier of L2 )
by FUNCT_2:def 1;
assume A7:
ex_inf_of X,[:L1,L2:]
; WAYBEL_0:def 30 ( ex_inf_of [:f,g:] .: X,[:T1,T2:] & "/\" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("/\" (X,[:L1,L2:])) )
then A8:
ex_inf_of proj1 X,L1
by YELLOW_3:42;
X c= the carrier of [:L1,L2:]
;
then A9:
X c= [: the carrier of L1, the carrier of L2:]
by YELLOW_3:def 2;
then A10:
proj2 ([:f,g:] .: X) = g .: (proj2 X)
by A6, Th4;
A11:
ex_inf_of proj2 X,L2
by A7, YELLOW_3:42;
then A12:
ex_inf_of proj2 ([:f,g:] .: X),T2
by A5, A10;
A13:
proj1 ([:f,g:] .: X) = f .: (proj1 X)
by A6, A9, Th4;
then
ex_inf_of proj1 ([:f,g:] .: X),T1
by A4, A8;
hence
ex_inf_of [:f,g:] .: X,[:T1,T2:]
by A12, YELLOW_3:42; "/\" (([:f,g:] .: X),[:T1,T2:]) = [:f,g:] . ("/\" (X,[:L1,L2:]))
hence inf ([:f,g:] .: X) =
[(inf (f .: (proj1 X))),(inf (g .: (proj2 X)))]
by A13, A10, Th7
.=
[(f . (inf (proj1 X))),(inf (g .: (proj2 X)))]
by A4, A8
.=
[(f . (inf (proj1 X))),(g . (inf (proj2 X)))]
by A5, A11
.=
[:f,g:] . ((inf (proj1 X)),(inf (proj2 X)))
by A6, FUNCT_3:def 8
.=
[:f,g:] . (inf X)
by A7, Th7
;
verum