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
let 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;
hence f1 = f2 ; :: thesis: verum