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)

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

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

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

per cases ( x in u or not x in u ) ;

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

then A4: not x in v by A1, XBOOLE_0:1;
A5: u @ x = 1. Z_2 by A3, Def3;
v @ x = 0. Z_2 by A4, Def3;
hence (u \+\ v) @ x = (u @ x) + (v @ x) by A2, A5, RLVECT_1:10; :: thesis: verum

end;

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

then A7: x in v by A1, XBOOLE_0:1;
A8: u @ x = 0. Z_2 by A6, Def3;
v @ x = 1. Z_2 by A7, Def3;
hence (u \+\ v) @ x = (u @ x) + (v @ x) by A2, A8, RLVECT_1:10; :: thesis: verum

end;

end;

end;

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

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

per cases ( x in u or not x in u ) ;

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

then A12: x in v by A9, XBOOLE_0:1;
u @ x = 1. Z_2 by A11, Def3;
hence (u \+\ v) @ x = (u @ x) + (v @ x) by A10, A12, Def3, Th7; :: thesis: verum

end;

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

then A14: not x in v by A9, XBOOLE_0:1;
A15: u @ x = 0. Z_2 by A13, Def3;
v @ x = 0. Z_2 by A14, Def3;
hence (u \+\ v) @ x = (u @ x) + (v @ x) by A10, A15, RLVECT_1:10; :: thesis: verum

end;

end;

end;

end;