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 "/\" (FinMeet B,f) = FinMeet B,(the L_meet 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 "/\" (FinMeet B,f) = FinMeet B,(the L_meet 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 "/\" (FinMeet B,f) = FinMeet B,(the L_meet 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 "/\" (FinMeet B,f) = FinMeet B,(the L_meet of L [;] v,f)
let f be Function of A,the carrier of L; :: thesis: ( B <> {} implies v "/\" (FinMeet B,f) = FinMeet B,(the L_meet of L [;] v,f) )
assume A1: B <> {} ; :: thesis: v "/\" (FinMeet B,f) = FinMeet B,(the L_meet of L [;] v,f)
set J = the L_meet of L;
the L_meet of L is idempotent ;
hence v "/\" (FinMeet B,f) = FinMeet B,(the L_meet of L [;] v,f) by A1, Th39, SETWISEO:36; :: thesis: verum