defpred S_{1}[ object , object ] means for h being Element of Subspaces VS st h = $1 holds

$2 = the carrier of h;

A1: for e being object st e in Subspaces VS holds

ex u being object st

( u in bool the carrier of VS & S_{1}[e,u] )

A4: for e being object st e in Subspaces VS holds

S_{1}[e,f . e]
from FUNCT_2:sch 1(A1);

take f ; :: thesis: for h being Element of Subspaces VS

for H being Subspace of VS st h = H holds

f . h = the carrier of H

thus for h being Element of Subspaces VS

for H being Subspace of VS st h = H holds

f . h = the carrier of H by A4; :: thesis: verum

$2 = the carrier of h;

A1: for e being object st e in Subspaces VS holds

ex u being object st

( u in bool the carrier of VS & S

proof

consider f being Function of (Subspaces VS),(bool the carrier of VS) such that
let e be object ; :: thesis: ( e in Subspaces VS implies ex u being object st

( u in bool the carrier of VS & S_{1}[e,u] ) )

assume A2: e in Subspaces VS ; :: thesis: ex u being object st

( u in bool the carrier of VS & S_{1}[e,u] )

then consider E being strict Subspace of VS such that

A3: E = e by VECTSP_5:def 3;

reconsider u = E as Element of Subspaces VS by A2, A3;

reconsider u1 = carr u as Subset of VS ;

take u1 ; :: thesis: ( u1 in bool the carrier of VS & S_{1}[e,u1] )

ex X being Subspace of VS st

( u = X & u1 = the carrier of X ) by Def3;

hence ( u1 in bool the carrier of VS & S_{1}[e,u1] )
by A3; :: thesis: verum

end;( u in bool the carrier of VS & S

assume A2: e in Subspaces VS ; :: thesis: ex u being object st

( u in bool the carrier of VS & S

then consider E being strict Subspace of VS such that

A3: E = e by VECTSP_5:def 3;

reconsider u = E as Element of Subspaces VS by A2, A3;

reconsider u1 = carr u as Subset of VS ;

take u1 ; :: thesis: ( u1 in bool the carrier of VS & S

ex X being Subspace of VS st

( u = X & u1 = the carrier of X ) by Def3;

hence ( u1 in bool the carrier of VS & S

A4: for e being object st e in Subspaces VS holds

S

take f ; :: thesis: for h being Element of Subspaces VS

for H being Subspace of VS st h = H holds

f . h = the carrier of H

thus for h being Element of Subspaces VS

for H being Subspace of VS st h = H holds

f . h = the carrier of H by A4; :: thesis: verum