let K be Ring; :: thesis: for G, F being non empty right_complementable add-associative right_zeroed ModuleStr over K

for x being Vector of [:G,F:]

for x1 being Vector of G

for x2 being Vector of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

let G, F be non empty right_complementable add-associative right_zeroed ModuleStr over K; :: thesis: for x being Vector of [:G,F:]

for x1 being Vector of G

for x2 being Vector of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

let x be Vector of [:G,F:]; :: thesis: for x1 being Vector of G

for x2 being Vector of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

let x1 be Vector of G; :: thesis: for x2 being Vector of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

let x2 be Vector of F; :: thesis: ( x = [x1,x2] implies - x = [(- x1),(- x2)] )

assume A1: x = [x1,x2] ; :: thesis: - x = [(- x1),(- x2)]

reconsider y = [(- x1),(- x2)] as Vector of [:G,F:] ;

x + y = [(x1 + (- x1)),(x2 + (- x2))] by A1, PRVECT_3:def 1

.= [(0. G),(x2 + (- x2))] by RLVECT_1:def 10

.= 0. [:G,F:] by RLVECT_1:def 10 ;

hence - x = [(- x1),(- x2)] by RLVECT_1:def 10; :: thesis: verum

for x being Vector of [:G,F:]

for x1 being Vector of G

for x2 being Vector of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

let G, F be non empty right_complementable add-associative right_zeroed ModuleStr over K; :: thesis: for x being Vector of [:G,F:]

for x1 being Vector of G

for x2 being Vector of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

let x be Vector of [:G,F:]; :: thesis: for x1 being Vector of G

for x2 being Vector of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

let x1 be Vector of G; :: thesis: for x2 being Vector of F st x = [x1,x2] holds

- x = [(- x1),(- x2)]

let x2 be Vector of F; :: thesis: ( x = [x1,x2] implies - x = [(- x1),(- x2)] )

assume A1: x = [x1,x2] ; :: thesis: - x = [(- x1),(- x2)]

reconsider y = [(- x1),(- x2)] as Vector of [:G,F:] ;

x + y = [(x1 + (- x1)),(x2 + (- x2))] by A1, PRVECT_3:def 1

.= [(0. G),(x2 + (- x2))] by RLVECT_1:def 10

.= 0. [:G,F:] by RLVECT_1:def 10 ;

hence - x = [(- x1),(- x2)] by RLVECT_1:def 10; :: thesis: verum