let X be finite Subset of NAT; :: thesis: Sum ((NAT --> 1) | X) = card X

per cases ( X = {} or X <> {} ) ;

suppose AA: X = {} ; :: thesis: Sum ((NAT --> 1) | X) = card X

then (NAT --> 1) | X = {}
.= X --> {} by AA ;
then (NAT --> 1) | X = EmptyMS X by PBOOLE:def 3;
then (NAT --> 1) | X = EmptyBag X ;
then A3: Sum ((NAT --> 1) | X) = 0 by UPROOTS:11;
card X = 0 by AA;
hence Sum ((NAT --> 1) | X) = card X by A3; :: thesis: verum

end;

suppose F1: X <> {} ; :: thesis: Sum ((NAT --> 1) | X) = card X

set f = NAT --> 1;
NAT c= REAL by NUMBERS:19;
then reconsider F = NAT --> 1 as PartFunc of NAT,REAL by FUNCT_2:7;
A1: Sum ((NAT --> 1) | X) = Sum (F,X) by NAT_5:25;
A2: Sum (F,X) = Sum (FinS (F,X)) by RFUNCT_3:def 14;
reconsider Z = dom (F | X) as finite set ;
f3: dom F = NAT ;
F | X = (X /\ NAT) --> 1 by FUNCOP_1:12
.= X --> 1 by XBOOLE_1:28 ;
then rng (F | X) = {1} by F1, FUNCOP_1:8;
then F2: Sum (FinS (F,X)) = Sum ((card Z) |-> 1) by RFUNCT_3:75;
Sum ((card Z) |-> 1) = 1 * (card Z) by ETRANS;
hence Sum ((NAT --> 1) | X) = card X by A1, A2, F2, f3; :: thesis: verum

end;

end;