defpred S1[ object , object ] means ex W being strict Subspace of M st
( $2 = W & $1 = the carrier of W );
defpred S2[ object ] means ex W being strict Subspace of M 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 M & S2[x] ) ) from XFAMILY:sch 1();
 A2: for x, y1, y2 being object st S1[x,y1] & S1[x,y2] holds
y1 = y2 by VECTSP_4:29;
consider f being Function such that
A3: for x, y being object holds
( [x,y] in f iff ( x in B & S1[x,y] ) ) from FUNCT_1:sch 1(A2);
 for x being object holds
( x in B iff ex y being object st [x,y] in f )
proof
let x be object ; :: thesis: ( x in B iff ex y being object st [x,y] in f )
thus ( x in B implies ex y being object st [x,y] in f ) :: thesis: ( ex y being object st [x,y] in f implies x in B )
proof
assume A4: x in B ; :: thesis: ex y being object st [x,y] in f
then consider W being strict Subspace of M such that
A5: x = the carrier of W by A1;
take W ; :: thesis: [x,W] in f
thus [x,W] in f by A3, A4, A5; :: thesis: verum
end;
thus ( ex y being object st [x,y] in f implies x in B ) by A3; :: thesis: verum
end;
then A6: B = dom f by XTUPLE_0:def 12;
for y being object holds
( y in rng f iff ex W being strict Subspace of M st y = W )
proof
let y be object ; :: thesis: ( y in rng f iff ex W being strict Subspace of M st y = W )
thus ( y in rng f implies ex W being strict Subspace of M st y = W ) :: thesis: ( ex W being strict Subspace of M st y = W implies y in rng f )
proof
assume y in rng f ; :: thesis: ex W being strict Subspace of M st y = W
then consider x being object such that
A7: ( x in dom f & y = f . x ) by FUNCT_1:def 3;
[x,y] in f by A7, FUNCT_1:def 2;
then ex W being strict Subspace of M st
( y = W & x = the carrier of W ) by A3;
hence ex W being strict Subspace of M st y = W ; :: thesis: verum
end;
given W being strict Subspace of M such that A8: y = W ; :: thesis: y in rng f
reconsider W = y as Subspace of M by A8;
reconsider x = the carrier of W as set ;
A9: y is set by TARSKI:1;
the carrier of W c= the carrier of M by VECTSP_4:def 2;
then A10: x in dom f by A1, A6, A8;
then [x,y] in f by A3, A6, A8;
then y = f . x by A10, FUNCT_1:def 2, A9;
hence y in rng f by A10, FUNCT_1:def 3; :: thesis: verum
end;
hence ex b1 being set st
for x being object holds
( x in b1 iff ex W being strict Subspace of M st W = x ) ; :: thesis: verum