let n be Nat; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for x being Element of L holds - (seq (n,x)) = seq (n,(- x))
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for x being Element of L holds - (seq (n,x)) = seq (n,(- x))
let x be Element of L; :: thesis: - (seq (n,x)) = seq (n,(- x))
let a be Element of NAT ; :: according to FUNCT_2:def 8 :: thesis: (- (seq (n,x))) . a = (seq (n,(- x))) . a
dom (- (seq (n,x))) = NAT by FUNCT_2:def 1;
then A1: (- (seq (n,x))) /. a = - ((seq (n,x)) /. a) by VFUNCT_1:def 5;

per cases ( a = n or a <> n ) ;

suppose a = n ; :: thesis: (- (seq (n,x))) . a = (seq (n,(- x))) . a

then ( (seq (n,x)) . a = x & (seq (n,(- x))) . a = - x ) by Th24;
hence (- (seq (n,x))) . a = (seq (n,(- x))) . a by A1; :: thesis: verum

end;

suppose a <> n ; :: thesis: (- (seq (n,x))) . a = (seq (n,(- x))) . a

then ( (seq (n,x)) . a = 0. L & (seq (n,(- x))) . a = 0. L ) by Th25;
hence (- (seq (n,x))) . a = (seq (n,(- x))) . a by A1; :: thesis: verum

end;

end;