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

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

hence
F1 = F2
by FUNCT_2:12; :: thesis: verum
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;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