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

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

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