let x, y, z, w be Real; :: thesis: for vx, vy being Element of REAL 2 st vx = <*x,y*> & vy = <*z,w*> holds
( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> )
let vx, vy be Element of REAL 2; :: thesis: ( vx = <*x,y*> & vy = <*z,w*> implies ( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> ) )
reconsider x1 = x, y1 = y, z1 = z, w1 = w as Element of REAL by XREAL_0:def 1;
assume A1: ( vx = <*x,y*> & vy = <*z,w*> ) ; :: thesis: ( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> )
hence vx + vy = <*(addreal . (x1,z1)),(addreal . (y1,w1))*> by FINSEQ_2:75
.= <*(x1 + z1),(addreal . (y1,w1))*> by BINOP_2:def 9
.= <*(x + z),(y + w)*> by BINOP_2:def 9 ;
:: thesis: vx - vy = <*(x - z),(y - w)*>
thus vx - vy = <*(diffreal . (x1,z1)),(diffreal . (y1,w1))*> by A1, FINSEQ_2:75
.= <*(x1 - z1),(diffreal . (y1,w1))*> by BINOP_2:def 10
.= <*(x - z),(y - w)*> by BINOP_2:def 10 ; :: thesis: verum