let A be non empty set ; :: thesis: for B being Element of Fin A
for L being D0_Lattice
for f being Function of A, the carrier of L
for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))
let B be Element of Fin A; :: thesis: for L being D0_Lattice
for f being Function of A, the carrier of L
for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))
let L be D0_Lattice; :: thesis: for f being Function of A, the carrier of L
for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))
let f be Function of A, the carrier of L; :: thesis: for u being Element of L holds the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))
let u be Element of L; :: thesis: the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f)))
A1: the L_meet of L . (u,(Bottom L)) = u "/\" (Bottom L)
.= Bottom L ;
( the L_meet of L is_distributive_wrt the L_join of L & Bottom L = the_unity_wrt the L_join of L ) by Th18, Th23;
hence the L_meet of L . (u,(FinJoin (B,f))) = FinJoin (B,( the L_meet of L [;] (u,f))) by A1, SETWOP_2:12; :: thesis: verum