let n be Nat; :: thesis: for x being Element of REAL n holds |(x,(0* n))| = 0
let x be Element of REAL n; :: thesis: |(x,(0* n))| = 0
|(x,(0* n))| = (1 / 4) * ((|.(x + (0* n)).| ^2 ) - (|.(x - (0* n)).| ^2 )) by EUCLID_2:10
.= (1 / 4) * ((|.x.| ^2 ) - (|.(x - (0* n)).| ^2 )) by Th1
.= (1 / 4) * ((|.x.| ^2 ) - (|.x.| ^2 )) by RVSUM_1:53
.= (1 / 4) * 0 ;
hence |(x,(0* n))| = 0 ; :: thesis: verum