let x be object ; :: thesis: for n being Nat
for r being Real st x in Seg n holds
|.((0* n) +* (x,r)).| = |.r.|
let n be Nat; :: thesis: for r being Real st x in Seg n holds
|.((0* n) +* (x,r)).| = |.r.|
let r be Real; :: thesis: ( 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 ; :: thesis: |.((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; :: thesis: verum