defpred S₁[ set ] means ex f being Function of V,V st
( f = $1 & f is isometric );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in Funcs the carrier of V,the carrier of V & S₁[x] ) ) from XBOOLE_0:sch 1();
take X ; :: thesis: for x being set holds
( x in X iff ex f being Function of V,V st
( f = x & f is isometric ) )
let x be set ; :: thesis: ( x in X iff ex f being Function of V,V st
( f = x & f is isometric ) )
thus ( x in X implies ex f being Function of V,V st
( f = x & f is isometric ) ) by A1; :: thesis: ( ex f being Function of V,V st
( f = x & f is isometric ) implies x in X )
thus ( ex f being Function of V,V st
( f = x & f is isometric ) implies x in X ) :: thesis: verum

proof

given f being Function of V,V such that A2: ( f = x & f is isometric ) ; :: thesis: x in X
f in Funcs the carrier of V,the carrier of V by FUNCT_2:11;
hence x in X by A1, A2; :: thesis: verum

end;