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 not x in v by A1, XBOOLE_0:1;
then A4: v @ x = 0. Z_2 by Def3;
u @ x = 1. Z_2 by A3, Def3;
hence (u \+\ v) @ x = (u @ x) + (v @ x) by A2, A4, RLVECT_1:4; :: thesis: verum

end;

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

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

end;

end;

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;

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

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

then ( x in v & u @ x = 1. Z_2 ) by A7, Def3, XBOOLE_0:1;
hence (u \+\ v) @ x = (u @ x) + (v @ x) by A8, Def3, Th7; :: thesis: verum

end;

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

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

end;

end;

end;

end;