let X be set ; :: thesis: for u, v being Subset of X

for x being Element of X holds (u \+\ v) @ x = (u @ x) + (v @ x)

let u, v be Subset of X; :: thesis: for x being Element of X holds (u \+\ v) @ x = (u @ x) + (v @ x)

let x be Element of X; :: thesis: (u \+\ v) @ x = (u @ x) + (v @ x)

for x being Element of X holds (u \+\ v) @ x = (u @ x) + (v @ x)

let u, v be Subset of X; :: thesis: for x being Element of X holds (u \+\ v) @ x = (u @ x) + (v @ x)

let x be Element of X; :: thesis: (u \+\ v) @ x = (u @ x) + (v @ x)

per cases
( x in u \+\ v or not x in u \+\ v )
;

end;

suppose A1:
x in u \+\ v
; :: thesis: (u \+\ v) @ x = (u @ x) + (v @ x)

then A2:
(u \+\ v) @ x = 1. Z_2
by Def3;

end;suppose A7:
not x in u \+\ v
; :: thesis: (u \+\ v) @ x = (u @ x) + (v @ x)

then A8:
(u \+\ v) @ x = 0. Z_2
by Def3;

end;