let F1, F2 be Function of the carrier of (lattice A), the carrier of (lattice B); :: thesis: ( ( for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
F1 . S = Lin B0 ) & ( for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
F2 . S = Lin B0 ) implies F1 = F2 )
assume that
A6: for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
F1 . S = Lin B0 and
A7: for S being strict Subspace of A
for B0 being Subset of B st B0 = f .: the carrier of S holds
F2 . S = Lin B0 ; :: thesis: F1 = F2
for h being object st h in the carrier of (lattice A) holds
F1 . h = F2 . h

proof

let h be object ; :: thesis: ( h in the carrier of (lattice A) implies F1 . h = F2 . h )
assume h in the carrier of (lattice A) ; :: thesis: F1 . h = F2 . h
then consider S being strict Subspace of A such that
A8: S = h by VECTSP_5:def 3;
reconsider B0 = f .: the carrier of S as Subset of B ;
F1 . h = Lin B0 by A6, A8;
hence F1 . h = F2 . h by A7, A8; :: thesis: verum

end;

hence F1 = F2 by FUNCT_2:12; :: thesis: verum