defpred S_{1}[ 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);

A4: for A being Element of CosetSet (V,W) holds S_{1}[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

$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_{1}[A,r]

consider f being Function of (CosetSet (V,W)),REAL such that let A be Element of CosetSet (V,W); :: thesis: ex r being Element of REAL st S_{1}[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_{1}[A,r]

thus S_{1}[A,r]
by A2, A3; :: thesis: verum

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

thus S

A4: for A being Element of CosetSet (V,W) holds S

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