let K be non empty right_complementable add-associative right_zeroed doubleLoopStr ; :: thesis: for x, y being Scalar of K
for a, b being Scalar of (opp K) st x = a & y = b holds
( x + y = a + b & x * y = b * a & - x = - a )
let x, y be Scalar of K; :: thesis: for a, b being Scalar of (opp K) st x = a & y = b holds
( x + y = a + b & x * y = b * a & - x = - a )
let a, b be Scalar of (opp K); :: thesis: ( x = a & y = b implies ( x + y = a + b & x * y = b * a & - x = - a ) )
assume that
A1: x = a and
A2: y = b ; :: thesis: ( x + y = a + b & x * y = b * a & - x = - a )
thus x + y = a + b by A1, A2; :: thesis: ( x * y = b * a & - x = - a )
thus x * y = b * a by A1, A2, FUNCT_4:def 8; :: thesis: - x = - a
reconsider c = - a as Element of K ;
c + x = (- a) + a by A1
.= 0. (opp K) by RLVECT_1:5
.= 0. K ;
hence - x = - a by RLVECT_1:6; :: thesis: verum