let n be Nat; :: thesis: for x being Element of REAL n holds
( |(x,x)| = 0 iff |.x.| = 0 )
let x be Element of REAL n; :: thesis: ( |(x,x)| = 0 iff |.x.| = 0 )
thus ( |(x,x)| = 0 implies |.x.| = 0 ) ; :: thesis: ( |.x.| = 0 implies |(x,x)| = 0 )
( |.x.| = 0 implies |(x,x)| = 0 ^2 ) by EUCLID_2:4;
hence ( |.x.| = 0 implies |(x,x)| = 0 ) ; :: thesis: verum