let X be RealUnitarySpace; :: thesis: for u being linear-Functional of X
for v being linear-Functional of (RUSp2RNSp X) st u = v holds
PreNorms u = PreNorms v
let u be linear-Functional of X; :: thesis: for v being linear-Functional of (RUSp2RNSp X) st u = v holds
PreNorms u = PreNorms v
let v be linear-Functional of (RUSp2RNSp X); :: thesis: ( u = v implies PreNorms u = PreNorms v )
assume AS: u = v ; :: thesis: PreNorms u = PreNorms v
set Y = RUSp2RNSp X;

A11: now :: thesis: for x being object st x in PreNorms u holds
x in PreNorms v

let x be object ; :: thesis: ( x in PreNorms u implies x in PreNorms v )
assume AS1: x in PreNorms u ; :: thesis: x in PreNorms v
then reconsider y = x as Real ;
consider t being VECTOR of X such that
B1: ( y = |.(u . t).| & ||.t.|| <= 1 ) by AS1;
reconsider t1 = t as VECTOR of (RUSp2RNSp X) ;
||.t1.|| <= 1 by B1, Def1;
hence x in PreNorms v by AS, B1; :: thesis: verum

end;

now :: thesis: for x being object st x in PreNorms v holds
x in PreNorms u

let x be object ; :: thesis: ( x in PreNorms v implies x in PreNorms u )
assume AS2: x in PreNorms v ; :: thesis: x in PreNorms u
then reconsider y = x as Real ;
consider t being VECTOR of (RUSp2RNSp X) such that
B1: ( y = |.(v . t).| & ||.t.|| <= 1 ) by AS2;
reconsider t1 = t as VECTOR of X ;
||.t1.|| <= 1 by B1, Def1;
hence x in PreNorms u by AS, B1; :: thesis: verum

end;

hence PreNorms u = PreNorms v by A11; :: thesis: verum