let F1, F2 be Function of (Subspaces VS),(bool the carrier of VS); :: thesis: ( ( for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
F1 . h = the carrier of H ) & ( for h being Element of Subspaces VS
for H being Subspace of VS st h = H holds
F2 . h = the carrier of H ) implies F1 = F2 )
assume that
A5: for h1 being Element of Subspaces VS
for H1 being Subspace of VS st h1 = H1 holds
F1 . h1 = the carrier of H1 and
A6: for h2 being Element of Subspaces VS
for H2 being Subspace of VS st h2 = H2 holds
F2 . h2 = the carrier of H2 ; :: thesis: F1 = F2
for h being object st h in Subspaces VS holds
F1 . h = F2 . h

proof

let h be object ; :: thesis: ( h in Subspaces VS implies F1 . h = F2 . h )
assume A7: h in Subspaces VS ; :: thesis: F1 . h = F2 . h
then h is Element of Subspaces VS ;
then consider H being Subspace of VS such that
A8: H = h ;
F1 . h = the carrier of H by A5, A7, A8;
hence F1 . h = F2 . h by A6, A7, A8; :: thesis: verum

end;

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