let A be non empty set ; for B being Element of Fin A
for L being D0_Lattice
for f, g being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) holds
u "/\" (FinJoin (B,f)) = FinJoin (B,g)
let B be Element of Fin A; for L being D0_Lattice
for f, g being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) holds
u "/\" (FinJoin (B,f)) = FinJoin (B,g)
let L be D0_Lattice; for f, g being Function of A, the carrier of L
for u being Element of L st ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) holds
u "/\" (FinJoin (B,f)) = FinJoin (B,g)
let f, g be Function of A, the carrier of L; for u being Element of L st ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) holds
u "/\" (FinJoin (B,f)) = FinJoin (B,g)
let u be Element of L; ( ( for x being Element of A st x in B holds
g . x = u "/\" (f . x) ) implies u "/\" (FinJoin (B,f)) = FinJoin (B,g) )
reconsider G = ( the L_meet of L [;] (u,f)) +* (g | B) as Function of A, the carrier of L by Th3;
dom (g | B) = B
by Th9;
then A1:
G | B = g | B
by FUNCT_4:23;
assume A2:
for x being Element of A st x in B holds
g . x = u "/\" (f . x)
; u "/\" (FinJoin (B,f)) = FinJoin (B,g)
then
G = the L_meet of L [;] (u,f)
by Th10;
hence u "/\" (FinJoin (B,f)) =
FinJoin (B,G)
by Th64
.=
FinJoin (B,g)
by A1, Th53
;
verum