let G, F be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for x being Point of [:G,F:]
for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
let x be Point of [:G,F:]; :: thesis: for x1 being Point of G
for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
let x1 be Point of G; :: thesis: for x2 being Point of F st x = [x1,x2] holds
- x = [(- x1),(- x2)]
let x2 be Point of F; :: thesis: ( x = [x1,x2] implies - x = [(- x1),(- x2)] )
assume A1: x = [x1,x2] ; :: thesis: - x = [(- x1),(- x2)]
reconsider y = [(- x1),(- x2)] as Point of [:G,F:] ;
x + y = [(x1 + (- x1)),(x2 + (- x2))] by A1, Def1
.= [(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