let n be set ; for L being non empty right_complementable add-associative right_zeroed doubleLoopStr
for a being Element of L holds - (a | (n,L)) = (- a) | (n,L)
let L be non empty right_complementable add-associative right_zeroed doubleLoopStr ; for a being Element of L holds - (a | (n,L)) = (- a) | (n,L)
let a be Element of L; - (a | (n,L)) = (- a) | (n,L)
dom (- (a | (n,L))) =
Bags n
by FUNCT_2:def 1
.=
dom ((- a) | (n,L))
by FUNCT_2:def 1
;
hence
- (a | (n,L)) = (- a) | (n,L)
by A1, FUNCT_1:2; verum