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

proof

let x be object ; :: 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 A1, 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 reconsider k = x as Element of NAT ;
A5: k in support (SMoebius X) by A4, Def5;
not x in Y /\ SCNAT by A2, A4, Lm1;
then A6: not k in support (SMoebius Y) by Def5;
(SMoebius (X \/ Y)) . x = (Moebius k) + 0 by A3, Def5
.= (Moebius k) + ((SMoebius Y) . k) by A6, PRE_POLY:def 7
.= ((SMoebius X) . k) + ((SMoebius Y) . k) by A5, Def5
.= ((SMoebius X) + (SMoebius Y)) . x by PRE_POLY: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 consider k being Element of NAT such that
A8: k = x ;
not x in X /\ SCNAT by A2, A7, Lm1;
then A9: not k in support (SMoebius X) by A8, Def5;
A10: k in support (SMoebius Y) by A7, A8, Def5;
(SMoebius (X \/ Y)) . x = (Moebius k) + 0 by A3, A8, Def5
.= (Moebius k) + ((SMoebius X) . k) by A9, PRE_POLY:def 7
.= ((SMoebius Y) . k) + ((SMoebius X) . k) by A10, Def5
.= ((SMoebius X) + (SMoebius Y)) . x by A8, PRE_POLY: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 Y /\ SCNAT by A1, XBOOLE_0:def 3;
then A12: not x in support (SMoebius Y) by Def5;
not x in X /\ SCNAT by A1, A11, XBOOLE_0:def 3;
then A13: not x in support (SMoebius X) by Def5;
(SMoebius (X \/ Y)) . x = 0 by A11, PRE_POLY:def 7
.= ((SMoebius Y) . x) + 0 by A12, PRE_POLY:def 7
.= ((SMoebius Y) . x) + ((SMoebius X) . x) by A13, PRE_POLY:def 7
.= ((SMoebius X) + (SMoebius Y)) . x by PRE_POLY: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