let L be Lattice; :: thesis: for A being non empty set
for B being Finite_Subset of A
for f, g being Function of A,the carrier of L st B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) holds
FinJoin B,f [= FinJoin B,g
let A be non empty set ; :: thesis: for B being Finite_Subset of A
for f, g being Function of A,the carrier of L st B <> {} & ( 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 Finite_Subset of A; :: thesis: for f, g being Function of A,the carrier of L st B <> {} & ( 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: ( B <> {} & ( for x being Element of A st x in B holds
f . x [= g . x ) implies FinJoin B,f [= FinJoin B,g )
assume that
A1: B <> {} and
A2: for x being Element of A st x in B holds
f . x [= g . x ; :: thesis: FinJoin B,f [= FinJoin B,g

now

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

end;

hence FinJoin B,f [= FinJoin B,g by A1, Th47; :: thesis: verum