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:
assume A4: x in support f ; :: thesis:
then A5: f . x <> 0 by PRE_POLY:def 7;

per cases ;

suppose S₁[x] ; :: thesis:

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

end;

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

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

end;

end;

end;

A6: support f = X /\ SCNAT

proof

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

proof

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

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A8: x in X /\ SCNAT ; :: thesis:
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:

end;

reconsider f = f as ManySortedSet of NAT ;
take f ; :: thesis:
thus support f = X /\ SCNAT by A6; :: thesis:
let k be Element of NAT ; :: thesis:
assume k in support f ; :: thesis:
hence f . k = Moebius k by A1, A6; :: thesis: