defpred S₁[ 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₁[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 & S₁[e,u] ) )
assume A2: e in Subspaces VS ; :: thesis: ex u being object st
( u in bool the carrier of VS & S₁[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₁[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₁[e,u1] ) by A3; :: thesis: verum

end;

consider f being Function of (Subspaces VS),(bool the carrier of VS) such that
A4: for e being object st e in Subspaces VS holds
S₁[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