let F1, F2 be Function of the carrier of (), the carrier of (); :: 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 () holds
F1 . h = F2 . h
proof
let h be object ; :: thesis: ( h in the carrier of () implies F1 . h = F2 . h )
assume h in the carrier of () ; :: 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