defpred S₁[ object , object ] means for i being Nat st i = $1 holds
$2 = card (f " {(i + 1)});
A1: for x being object st x in n holds
ex y being object st
( y in NAT & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in n implies ex y being object st
( y in NAT & S₁[x,y] ) )
assume A2: x in n ; :: thesis: ex y being object st
( y in NAT & S₁[x,y] )
x in Segm n by A2;
then reconsider x = x as Nat ;
take c = card (f " {(x + 1)}); :: thesis: ( c in NAT & S₁[x,c] )
thus ( c in NAT & S₁[x,c] ) ; :: thesis: verum

end;

consider c being Function such that
A3: ( dom c = n & rng c c= NAT & ( for x being object st x in n holds
S₁[x,c . x] ) ) from FUNCT_1:sch 6(A1);
reconsider c = c as ManySortedSet of n by A3, PARTFUN1:def 2, RELAT_1:def 18;
reconsider c = c as bag of n by A3, VALUED_0:def 6;
take c ; :: thesis: for i being Nat st i in n holds
c . i = card (f " {(i + 1)})
let i be Nat; :: thesis: ( i in n implies c . i = card (f " {(i + 1)}) )
assume i in n ; :: thesis: c . i = card (f " {(i + 1)})
hence c . i = card (f " {(i + 1)}) by A3; :: thesis: verum