defpred S_{1}[ object , object ] means ex W being strict Subspace of V st

( $2 = W & $1 = the carrier of W );

defpred S_{2}[ 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_{2}[x] ) )
from XFAMILY:sch 1();

A2: for x, y1, y2 being object st S_{1}[x,y1] & S_{1}[x,y2] holds

y1 = y2 by RLSUB_1:30;

consider f being Function such that

A3: for x, y being object holds

( [x,y] in f iff ( x in B & S_{1}[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 )

for y being object holds

( y in rng f iff y is strict Subspace of V )_{1} being set st

for x being object holds

( x in b_{1} iff x is strict Subspace of V )
; :: thesis: verum

( $2 = W & $1 = the carrier of W );

defpred S

consider B being set such that

A1: for x being set holds

( x in B iff ( x in bool the carrier of V & S

A2: for x, y1, y2 being object st S

y1 = y2 by RLSUB_1:30;

consider f being Function such that

A3: for x, y being object holds

( [x,y] in f iff ( x in B & S

for x being object holds

( x in B iff ex y being object st [x,y] in f )

proof

then A6:
B = dom f
by XTUPLE_0:def 12;
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 )

end;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

thus
( ex y being object st [x,y] in f implies x in B )
by A3; :: thesis: verum
assume A4:
x in B
; :: thesis: ex y being object st [x,y] in f

then consider W being strict Subspace of V 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;then consider W being strict Subspace of V 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

for y being object holds

( y in rng f iff y is strict Subspace of V )

proof

hence
ex b
let y be object ; :: 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 )

then reconsider W = y as strict Subspace of V ;

A8: y is set by TARSKI:1;

reconsider x = the carrier of W as set ;

the carrier of W c= the carrier of V by RLSUB_1:def 2;

then A9: x in dom f by A1, A6;

then [x,y] in f by A3, A6;

then y = f . x by A9, FUNCT_1:def 2, A8;

hence y in rng f by A9, FUNCT_1:def 3; :: thesis: verum

end;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 is strict Subspace of V
; :: thesis: y in rng f
assume
y in rng f
; :: thesis: y is strict Subspace of V

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 V st

( y = W & x = the carrier of W ) by A3;

hence y is strict Subspace of V ; :: thesis: verum

end;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 V st

( y = W & x = the carrier of W ) by A3;

hence y is strict Subspace of V ; :: thesis: verum

then reconsider W = y as strict Subspace of V ;

A8: y is set by TARSKI:1;

reconsider x = the carrier of W as set ;

the carrier of W c= the carrier of V by RLSUB_1:def 2;

then A9: x in dom f by A1, A6;

then [x,y] in f by A3, A6;

then y = f . x by A9, FUNCT_1:def 2, A8;

hence y in rng f by A9, FUNCT_1:def 3; :: thesis: verum

for x being object holds

( x in b