defpred S₁[ object ] means $1 in X /\ SCNAT;
deffunc H₁( Element of NAT ) -> Element of NAT = 0 ;
deffunc H₂( Element of NAT ) -> Real = Moebius $1;
ex f being ManySortedSet of NAT st
for i being Element of NAT st i in NAT holds
( ( S₁[i] implies f . i = H₂(i) ) & ( not S₁[i] implies f . i = H₁(i) ) ) from PRE_CIRC:sch 2();
then consider f being ManySortedSet of NAT such that
A1: for i being Element of NAT st i in NAT holds
( ( S₁[i] implies f . i = H₂(i) ) & ( not S₁[i] implies f . i = H₁(i) ) ) ;
A2: support f c= SCNAT

proof

dom f = NAT by PARTFUN1:def 2;
then A3: support f c= NAT by PRE_POLY:37;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support f or x in SCNAT )
assume A4: x in support f ; :: thesis: x in SCNAT
then A5: f . x <> 0 by PRE_POLY:def 7;

per cases ( S₁[x] or not S₁[x] ) ;

suppose S₁[x] ; :: thesis: x in SCNAT

hence x in SCNAT by XBOOLE_0:def 4; :: thesis: verum

end;

suppose not S₁[x] ; :: thesis: x in SCNAT

hence x in SCNAT by A1, A4, A5, A3; :: thesis: verum

end;

end;

end;

A6: support f = X /\ SCNAT

proof

thus support f c= X /\ SCNAT :: according to XBOOLE_0:def 10 :: thesis: X /\ SCNAT c= support f

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support f or x in X /\ SCNAT )
assume A7: x in support f ; :: thesis: x in X /\ SCNAT
then x in SCNAT by A2;
then reconsider i = x as Element of NAT ;
assume not x in X /\ SCNAT ; :: thesis: contradiction
then f . i = 0 by A1;
hence contradiction by A7, PRE_POLY:def 7; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X /\ SCNAT or x in support f )
assume A8: x in X /\ SCNAT ; :: thesis: x in support f
then reconsider i = x as Element of NAT ;
x in SCNAT by A8, XBOOLE_0:def 4;
then A9: Moebius i <> 0 by Th38;
f . i = Moebius i by A1, A8;
hence x in support f by A9, PRE_POLY:def 7; :: thesis: verum

end;

reconsider f = f as ManySortedSet of NAT ;
take f ; :: thesis: ( support f = X /\ SCNAT & ( for k being Nat st k in support f holds
f . k = Moebius k ) )
thus ( support f = X /\ SCNAT & ( for k being Nat st k in support f holds
f . k = Moebius k ) ) by A1, A6; :: thesis: verum