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

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