let x be object ; for n being Nat
for r being Real st x in Seg n holds
|.((0* n) +* (x,r)).| = |.r.|
let n be Nat; for r being Real st x in Seg n holds
|.((0* n) +* (x,r)).| = |.r.|
let r be Real; ( x in Seg n implies |.((0* n) +* (x,r)).| = |.r.| )
set f = (0* n) +* (x,r);
A1:
n in NAT
by ORDINAL1:def 12;
assume A2:
x in Seg n
; |.((0* n) +* (x,r)).| = |.r.|
((0* n) +* (x,r)) ^2 = (0* n) +* (x,(r ^2))
by Th12;
then
Sum (((0* n) +* (x,r)) ^2) = r ^2
by A2, A1, JORDAN2B:10;
hence
|.((0* n) +* (x,r)).| = |.r.|
by COMPLEX1:72; verum