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 12;
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:10;
hence |.((0* n) +* (x,r)).| = abs r by COMPLEX1:72; :: thesis: verum