let X, Y be finite Subset of NAT ; :: thesis: ( X misses Y implies SMoebius (X \/ Y) = (SMoebius X) + (SMoebius Y) )
assume A1: X misses Y ; :: thesis: SMoebius (X \/ Y) = (SMoebius X) + (SMoebius Y)
A2: support (SMoebius (X \/ Y)) = (X \/ Y) /\ SCNAT by Def5
.= (X /\ SCNAT ) \/ (Y /\ SCNAT ) by XBOOLE_1:23 ;
for x being set st x in NAT holds
(SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x

proof

let x be set ; :: thesis: ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x )

per cases ( x in support (SMoebius (X \/ Y)) or not x in support (SMoebius (X \/ Y)) ) ;

suppose A3: x in support (SMoebius (X \/ Y)) ; :: thesis: ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x )

per cases ( x in X /\ SCNAT or x in Y /\ SCNAT ) by A2, A3, XBOOLE_0:def 3;

suppose A4: x in X /\ SCNAT ; :: thesis: ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x )

then A5: not x in Y /\ SCNAT by A1, Lm1;
reconsider k = x as Element of NAT by A4;
A6: ( k in support (SMoebius X) & not k in support (SMoebius Y) ) by A4, A5, Def5;
(SMoebius (X \/ Y)) . x = (Moebius k) + 0 by A3, Def5
.= (Moebius k) + ((SMoebius Y) . k) by A6, POLYNOM1:def 7
.= ((SMoebius X) . k) + ((SMoebius Y) . k) by A6, Def5
.= ((SMoebius X) + (SMoebius Y)) . x by POLYNOM1:def 5 ;
hence ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x ) ; :: thesis: verum

end;

suppose A7: x in Y /\ SCNAT ; :: thesis: ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x )

then A8: not x in X /\ SCNAT by A1, Lm1;
consider k being Element of NAT such that
A9: k = x by A7;
A10: ( k in support (SMoebius Y) & not k in support (SMoebius X) ) by A7, A8, A9, Def5;
(SMoebius (X \/ Y)) . x = (Moebius k) + 0 by A3, A9, Def5
.= (Moebius k) + ((SMoebius X) . k) by A10, POLYNOM1:def 7
.= ((SMoebius Y) . k) + ((SMoebius X) . k) by A10, Def5
.= ((SMoebius X) + (SMoebius Y)) . x by A9, POLYNOM1:def 5 ;
hence ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x ) ; :: thesis: verum

end;

end;

end;

suppose A11: not x in support (SMoebius (X \/ Y)) ; :: thesis: ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x )

then ( not x in X /\ SCNAT & not x in Y /\ SCNAT ) by A2, XBOOLE_0:def 3;
then A12: ( not x in support (SMoebius X) & not x in support (SMoebius Y) ) by Def5;
(SMoebius (X \/ Y)) . x = 0 by A11, POLYNOM1:def 7
.= ((SMoebius Y) . x) + 0 by A12, POLYNOM1:def 7
.= ((SMoebius Y) . x) + ((SMoebius X) . x) by A12, POLYNOM1:def 7
.= ((SMoebius X) + (SMoebius Y)) . x by POLYNOM1:def 5 ;
hence ( x in NAT implies (SMoebius (X \/ Y)) . x = ((SMoebius X) + (SMoebius Y)) . x ) ; :: thesis: verum

end;

end;

end;

hence SMoebius (X \/ Y) = (SMoebius X) + (SMoebius Y) by PBOOLE:3; :: thesis: verum