let A be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: FinJoin (B,f) [= FinJoin (B,g)

now :: thesis: for x being Element of A st x in B holds
f . x [= FinJoin (B,g)

let x be Element of A; :: thesis: ( x in B implies f . x [= FinJoin (B,g) )
assume A2: x in B ; :: thesis: f . x [= FinJoin (B,g)
then f . x [= g . x by A1;
hence f . x [= FinJoin (B,g) by A2, Th29; :: thesis: verum

end;

hence FinJoin (B,f) [= FinJoin (B,g) by Th54; :: thesis: verum