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:3
.= (1 / 4) * ((|.x.| ^2) - (|.(x - (0* n)).| ^2)) by Th1
.= (1 / 4) * ((|.x.| ^2) - (|.x.| ^2)) by RVSUM_1:32
.= (1 / 4) * 0 ;
hence |(x,(0* n))| = 0 ; :: thesis: verum