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

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