let A be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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) ; :: thesis: u "/\" (FinJoin (B,f)) = FinJoin (B,g)

now :: thesis: for x being Element of A st x in B holds
g . x = ( the L_meet of L [;] (u,f)) . x

let x be Element of A; :: thesis: ( x in B implies g . x = ( the L_meet of L [;] (u,f)) . x )
assume x in B ; :: thesis: g . x = ( the L_meet of L [;] (u,f)) . x
hence g . x = u "/\" (f . x) by A2
.= ( the L_meet of L [;] (u,f)) . x by FUNCOP_1:53 ;
:: thesis: verum

end;

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 ;
:: thesis: verum