let x be set ; :: thesis: for n being Nat
for r being real number st x in Seg n holds
|.((0* n) +* x,r).| = abs r
let n be Nat; :: thesis: for r being real number st x in Seg n holds
|.((0* n) +* x,r).| = abs r
let r be real number ; :: thesis: ( x in Seg n implies |.((0* n) +* x,r).| = abs r )
set f = (0* n) +* x,r;
A1: r ^2 in REAL by XREAL_0:def 1;
A2: n in NAT by ORDINAL1:def 13;
assume A3: x in Seg n ; :: thesis: |.((0* n) +* x,r).| = abs r
((0* n) +* x,r) ^2 = (0* n) +* x,(r ^2 ) by Th12;
then Sum (((0* n) +* x,r) ^2 ) = r ^2 by A3, A1, A2, JORDAN2B:14;
hence |.((0* n) +* x,r).| = abs r by COMPLEX1:158; :: thesis: verum