let n be Nat; :: thesis: for L being non empty right_complementable add-associative right_zeroed addLoopStr
for x, y being Element of L holds (seq (n,x)) - (seq (n,y)) = seq (n,(x - y))
let L be non empty right_complementable add-associative right_zeroed addLoopStr ; :: thesis: for x, y being Element of L holds (seq (n,x)) - (seq (n,y)) = seq (n,(x - y))
let x, y be Element of L; :: thesis: (seq (n,x)) - (seq (n,y)) = seq (n,(x - y))
thus (seq (n,x)) - (seq (n,y)) = (seq (n,x)) + (seq (n,(- y))) by Th30
.= seq (n,(x - y)) by Th29 ; :: thesis: verum