let L be Lattice; :: thesis: for v being Element of L
for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st B <> {} holds
v "\/" (FinJoin B,f) = FinJoin B,(the L_join of L [;] v,f)
let v be Element of L; :: thesis: for A being non empty set
for B being Finite_Subset of A
for f being Function of A,the carrier of L st B <> {} holds
v "\/" (FinJoin B,f) = FinJoin B,(the L_join of L [;] v,f)
let A be non empty set ; :: thesis: for B being Finite_Subset of A
for f being Function of A,the carrier of L st B <> {} holds
v "\/" (FinJoin B,f) = FinJoin B,(the L_join of L [;] v,f)
let B be Finite_Subset of A; :: thesis: for f being Function of A,the carrier of L st B <> {} holds
v "\/" (FinJoin B,f) = FinJoin B,(the L_join of L [;] v,f)
let f be Function of A,the carrier of L; :: thesis: ( B <> {} implies v "\/" (FinJoin B,f) = FinJoin B,(the L_join of L [;] v,f) )
assume A1: B <> {} ; :: thesis: v "\/" (FinJoin B,f) = FinJoin B,(the L_join of L [;] v,f)
set J = the L_join of L;
the L_join of L is idempotent by Th26;
hence v "\/" (FinJoin B,f) = FinJoin B,(the L_join of L [;] v,f) by A1, Th34, SETWISEO:36; :: thesis: verum