theorem Th10: :: REAL_NS1:10

for n being Nat
for x being Element of REAL (n + 1) holds |.x.| ^2 = (|.(x | n).| ^2) + ((x . (n + 1)) ^2)