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 ;
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:89
.= <*(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:89
.= <*(x1 - z1),(diffreal . y1,w1)*> by BINOP_2:def 10
.= <*(x - z),(y - w)*> by BINOP_2:def 10 ; :: thesis: verum