let A be non empty set ; :: thesis: for B being Finite_Subset of A
for L being D0_Lattice
for g, f 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 Finite_Subset of A; :: thesis: for L being D0_Lattice
for g, f 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 g, f 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 g, f 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 Th6;
dom (g | B) = B by Th13;
then A1: G | B = g | B by FUNCT_4:24;
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

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

end;

then G = the L_meet of L [;] u,f by Th14;
hence u "/\" (FinJoin B,f) = FinJoin B,G by Th81
.= FinJoin B,g by A1, Th69 ;
:: thesis: verum