let A be non empty set ; :: thesis: for B being Finite_Subset of A
for L being 1_Lattice
for f, g being Function of A, the carrier of L st f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
let B be Finite_Subset of A; :: thesis: for L being 1_Lattice
for f, g being Function of A, the carrier of L st f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
let L be 1_Lattice; :: thesis: for f, g being Function of A, the carrier of L st f | B = g | B holds
FinMeet (B,f) = FinMeet (B,g)
let f, g be Function of A, the carrier of L; :: thesis: ( f | B = g | B implies FinMeet (B,f) = FinMeet (B,g) )
assume A1: f | B = g | B ; :: thesis: FinMeet (B,f) = FinMeet (B,g)
reconsider f9 = f, g9 = g as Function of A, the carrier of (L .:) ;
A2: FinMeet (B,g) = FinJoin (B,g9) ;
( L .: is 0_Lattice & FinMeet (B,f) = FinJoin (B,f9) ) by Th64;
hence FinMeet (B,f) = FinMeet (B,g) by A1, A2, Th69; :: thesis: verum