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

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