set C = CosetSet (V,W);

let f1, f2 be Function of (CosetSet (V,W)),REAL; :: thesis: ( ( for A being Element of CosetSet (V,W)

for v being VECTOR of V st A = v + W holds

f1 . A = lower_bound (NormVSets (V,W,v)) ) & ( for A being Element of CosetSet (V,W)

for v being VECTOR of V st A = v + W holds

f2 . A = lower_bound (NormVSets (V,W,v)) ) implies f1 = f2 )

assume that

A5: for A being Element of CosetSet (V,W)

for a being VECTOR of V st A = a + W holds

f1 . A = lower_bound (NormVSets (V,W,a)) and

A6: for A being Element of CosetSet (V,W)

for a being VECTOR of V st A = a + W holds

f2 . A = lower_bound (NormVSets (V,W,a)) ; :: thesis: f1 = f2

set C = CosetSet (V,W);

let f1, f2 be Function of (CosetSet (V,W)),REAL; :: thesis: ( ( for A being Element of CosetSet (V,W)

for v being VECTOR of V st A = v + W holds

f1 . A = lower_bound (NormVSets (V,W,v)) ) & ( for A being Element of CosetSet (V,W)

for v being VECTOR of V st A = v + W holds

f2 . A = lower_bound (NormVSets (V,W,v)) ) implies f1 = f2 )

assume that

A5: for A being Element of CosetSet (V,W)

for a being VECTOR of V st A = a + W holds

f1 . A = lower_bound (NormVSets (V,W,a)) and

A6: for A being Element of CosetSet (V,W)

for a being VECTOR of V st A = a + W holds

f2 . A = lower_bound (NormVSets (V,W,a)) ; :: thesis: f1 = f2

set C = CosetSet (V,W);

now :: thesis: for A being Element of CosetSet (V,W) holds f1 . A = f2 . A

hence
f1 = f2
; :: thesis: verumlet A be Element of CosetSet (V,W); :: thesis: f1 . A = f2 . A

A in CosetSet (V,W) ;

then consider A1 being Coset of W such that

A7: A1 = A ;

consider a being VECTOR of V such that

A8: A1 = a + W by RLSUB_1:def 6;

thus f1 . A = lower_bound (NormVSets (V,W,a)) by A5, A7, A8

.= f2 . A by A6, A7, A8 ; :: thesis: verum

end;A in CosetSet (V,W) ;

then consider A1 being Coset of W such that

A7: A1 = A ;

consider a being VECTOR of V such that

A8: A1 = a + W by RLSUB_1:def 6;

thus f1 . A = lower_bound (NormVSets (V,W,a)) by A5, A7, A8

.= f2 . A by A6, A7, A8 ; :: thesis: verum