let A be non empty set ; :: thesis:
let B be Finite_Subset of A; :: thesis:
let L be 0_Lattice; :: thesis:
let f, g be Function of A,the carrier of L; :: thesis:
assume A1: for x being Element of A st x in B holds
f . x [= g . x ; :: thesis:

end;