let L be Lattice; :: thesis: for A being non empty set
for B being Element of Fin A
for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
let A be non empty set ; :: thesis: for B being Element of Fin A
for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
let B be Element of Fin A; :: thesis: for f, g being Function of A, the carrier of L st B <> {} & f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
let f, g be Function of A, the carrier of L; :: thesis: ( B <> {} & f | B = g | B implies FinMeet (B,f) = FinMeet (B,g) )
reconsider f9 = f, g9 = g as Function of A, the carrier of (L .:) ;
A1: ( FinMeet (B,f) = FinJoin (B,f9) & FinMeet (B,g) = FinJoin (B,g9) ) ;
assume ( B <> {} & f | B = g | B ) ; :: thesis: FinMeet (B,f) = FinMeet (B,g)
hence FinMeet (B,f) = FinMeet (B,g) by A1, Th34; :: thesis: verum