defpred S₁[ set , set ] means ex W being strict Subspace of V st
( $2 = W & $1 = the carrier of W );
defpred S₂[ set ] means ex W being strict Subspace of V st $1 = the carrier of W;
consider B being set such that
A1: for x being set holds
( x in B iff ( x in bool the carrier of V & S₂[x] ) ) from XBOOLE_0:sch 1();
A2: for x, y1, y2 being set st S₁[x,y1] & S₁[x,y2] holds
y1 = y2 by RUSUB_1:24;
consider f being Function such that
A3: for x, y being set holds
( [x,y] in f iff ( x in B & S₁[x,y] ) ) from FUNCT_1:sch 1(A2);
for x being set holds
( x in B iff ex y being set st [x,y] in f )

proof

let x be set ; :: thesis: ( x in B iff ex y being set st [x,y] in f )
thus ( x in B implies ex y being set st [x,y] in f ) :: thesis: ( ex y being set st [x,y] in f implies x in B )

proof

assume A4: x in B ; :: thesis: ex y being set st [x,y] in f
then consider W being strict Subspace of V such that
A5: x = the carrier of W by A1;
reconsider y = W as set ;
take y ; :: thesis: [x,y] in f
thus [x,y] in f by A3, A4, A5; :: thesis: verum

end;

given y being set such that A6: [x,y] in f ; :: thesis: x in B
thus x in B by A3, A6; :: thesis: verum

end;

then A7: B = dom f by RELAT_1:def 4;
for y being set holds
( y in rng f iff y is strict Subspace of V )

proof

let y be set ; :: thesis: ( y in rng f iff y is strict Subspace of V )
thus ( y in rng f implies y is strict Subspace of V ) :: thesis: ( y is strict Subspace of V implies y in rng f )

proof

assume y in rng f ; :: thesis: y is strict Subspace of V
then consider x being set such that
A8: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
[x,y] in f by A8, FUNCT_1:def 2;
then ex W being strict Subspace of V st
( y = W & x = the carrier of W ) by A3;
hence y is strict Subspace of V ; :: thesis: verum

end;

assume y is strict Subspace of V ; :: thesis: y in rng f
then reconsider W = y as strict Subspace of V ;
reconsider x = the carrier of W as set ;
the carrier of W c= the carrier of V by RUSUB_1:def 1;
then A9: x in dom f by A1, A7;
then [x,y] in f by A3, A7;
then y = f . x by A9, FUNCT_1:def 2;
hence y in rng f by A9, FUNCT_1:def 3; :: thesis: verum

end;

hence ex b₁ being set st
for x being set holds
( x in b₁ iff x is strict Subspace of V ) ; :: thesis: verum