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
FinJoin (B,f) = FinJoin (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
FinJoin (B,f) = FinJoin (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
FinJoin (B,f) = FinJoin (B,g)
let f, g be Function of A, the carrier of L; :: thesis: ( B <> {} & f | B = g | B implies FinJoin (B,f) = FinJoin (B,g) )
assume that
A1: B <> {} and
A2: f | B = g | B ; :: thesis: FinJoin (B,f) = FinJoin (B,g)
f .: B = g .: B by A2, RELAT_1:166;
hence FinJoin (B,f) = FinJoin (B,g) by A1, SETWISEO:26; :: thesis: verum