let A be non empty set ; for B being Element of Fin A
for L being 0_Lattice
for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin (B,f) [= FinJoin (B,g)
let B be Element of Fin A; for L being 0_Lattice
for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin (B,f) [= FinJoin (B,g)
let L be 0_Lattice; for f, g being Function of A, the carrier of L st ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin (B,f) [= FinJoin (B,g)
let f, g be Function of A, the carrier of L; ( ( for x being Element of A st x in B holds
f . x [= g . x ) implies FinJoin (B,f) [= FinJoin (B,g) )
assume A1:
for x being Element of A st x in B holds
f . x [= g . x
; FinJoin (B,f) [= FinJoin (B,g)
hence
FinJoin (B,f) [= FinJoin (B,g)
by Th54; verum