defpred S₁[ 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 S₁[A,r]

let A be Element of CosetSet (V,W); :: thesis: ex r being Element of REAL st S₁[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: S₁[A,r]
thus S₁[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 S₁[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