let X, Y be RealNormSpace; :: thesis: for x being Point of X
for y being Point of Y
for z being Point of [:X,Y:] st z = [x,y] holds
||.z.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2))
let x be Point of X; :: thesis: for y being Point of Y
for z being Point of [:X,Y:] st z = [x,y] holds
||.z.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2))
let y be Point of Y; :: thesis: for z being Point of [:X,Y:] st z = [x,y] holds
||.z.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2))
let z be Point of [:X,Y:]; :: thesis: ( z = [x,y] implies ||.z.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2)) )
assume z = [x,y] ; :: thesis: ||.z.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2))
then consider w being Element of REAL 2 such that
A1: ( w = <*||.x.||,||.y.||*> & ||.z.|| = |.w.| ) by PRVECT_3:18;
w in 2 -tuples_on REAL ;
then A2: ex s being Element of REAL * st
( s = w & len s = 2 ) ;
( w . 1 = ||.x.|| & w . 2 = ||.y.|| ) by A1, FINSEQ_1:44;
hence ||.z.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2)) by A1, A2, EUCLID_3:22; :: thesis: verum