defpred S1[ set , set ] means for v being VECTOR of V st $1 = v + W holds
$2 = lower_bound (NormVSets (V,W,v));
set C = CosetSet (V,W);
A1: now :: thesis: for A being Element of CosetSet (V,W) ex r being Element of REAL st S1[A,r]
let A be Element of CosetSet (V,W); :: thesis: ex r being Element of REAL st S1[A,r]
A in CosetSet (V,W) ;
then consider A1 being Coset of W such that
A2: A1 = A ;
consider v0 being VECTOR of V such that
A3: A1 = v0 + W by RLSUB_1:def 6;
reconsider r = lower_bound (NormVSets (V,W,v0)) as Element of REAL by XREAL_0:def 1;
take r = r; :: thesis: S1[A,r]
thus S1[A,r] by A2, A3; :: thesis: verum
end;
consider f being Function of (CosetSet (V,W)),REAL such that
A4: for A being Element of CosetSet (V,W) holds S1[A,f . A] from FUNCT_2:sch 3(A1);
 take f ; :: thesis: for A being Element of CosetSet (V,W)
for v being VECTOR of V st A = v + W holds
f . A = lower_bound (NormVSets (V,W,v))
let A be Element of CosetSet (V,W); :: thesis: for v being VECTOR of V st A = v + W holds
f . A = lower_bound (NormVSets (V,W,v))
let v be VECTOR of V; :: thesis: ( A = v + W implies f . A = lower_bound (NormVSets (V,W,v)) )
assume A = v + W ; :: thesis: f . A = lower_bound (NormVSets (V,W,v))
hence f . A = lower_bound (NormVSets (V,W,v)) by A4; :: thesis: verum