let L be Lattice; :: thesis:
let A be non empty set ; :: thesis:
let B be Finite_Subset of A; :: thesis:
let f, g be Function of A, the carrier of L; :: thesis:
assume that
A1: B <> {} and
A2: for x being Element of A st x in B holds
f . x [= g . x ; :: thesis:

end;