defpred S1[ 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 & S1[e,u] )
proof
let e be object ; :: thesis: ( e in Subspaces VS implies ex u being object st
( u in bool the carrier of VS & S1[e,u] ) )

assume A2: e in Subspaces VS ; :: thesis: ex u being object st
( u in bool the carrier of VS & S1[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 & S1[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 & S1[e,u1] ) by A3; :: thesis: verum
end;
consider f being Function of (),(bool the carrier of VS) such that
A4: for e being object st e in Subspaces VS holds
S1[e,f . e] from 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