defpred S1[ Nat] means for D being finite set st card D = $1 holds
for f being Function of D,NAT ex h being FinSequence of D st
for d being Element of D holds card (Coim (h,d)) = f . d;
A1:
S1[ 0 ]
proof
let D be
finite set ;
( card D = 0 implies for f being Function of D,NAT ex h being FinSequence of D st
for d being Element of D holds card (Coim (h,d)) = f . d )
assume A2:
card D = 0
;
for f being Function of D,NAT ex h being FinSequence of D st
for d being Element of D holds card (Coim (h,d)) = f . d
let f be
Function of
D,
NAT;
ex h being FinSequence of D st
for d being Element of D holds card (Coim (h,d)) = f . d
take h =
<*> D;
for d being Element of D holds card (Coim (h,d)) = f . d
let d be
Element of
D;
card (Coim (h,d)) = f . d
A3:
Coim (
h,
d)
= h " {d}
by RELAT_1:def 17;
not
d in dom f
by A2;
hence
card (Coim (h,d)) = f . d
by FUNCT_1:def 2, A3;
verum
end;
A4:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A5:
S1[
i]
;
S1[i + 1]
set i1 =
i + 1;
let D be
finite set ;
( card D = i + 1 implies for f being Function of D,NAT ex h being FinSequence of D st
for d being Element of D holds card (Coim (h,d)) = f . d )
assume A6:
card D = i + 1
;
for f being Function of D,NAT ex h being FinSequence of D st
for d being Element of D holds card (Coim (h,d)) = f . d
let f be
Function of
D,
NAT;
ex h being FinSequence of D st
for d being Element of D holds card (Coim (h,d)) = f . d
not
D is
empty
by A6;
then consider d being
object such that A7:
d in D
;
set Dd =
D \ {d};
A8:
card (D \ {d}) = i
by A6, A7, STIRL2_1:55;
reconsider fd =
f | (D \ {d}) as
Function of
(D \ {d}),
NAT ;
consider h being
FinSequence of
D \ {d} such that A9:
for
x being
Element of
D \ {d} holds
card (Coim (h,x)) = fd . x
by A5, A8;
A10:
rng h c= D \ {d}
;
D \ {d} c= D
;
then
rng h c= D
;
then reconsider h =
h as
FinSequence of
D by FINSEQ_1:def 4;
reconsider g =
(f . d) |-> d as
FinSequence of
D by A7, FINSEQ_2:63;
take hg =
h ^ g;
for d being Element of D holds card (Coim (hg,d)) = f . d
let x be
Element of
D;
card (Coim (hg,x)) = f . x
(
Coim (
hg,
x)
= hg " {x} &
Coim (
h,
x)
= h " {x} &
Coim (
g,
x)
= g " {x} )
by RELAT_1:def 17;
then A11:
card (Coim (hg,x)) = (card (h " {x})) + (card (g " {x}))
by FINSEQ_3:57;
end;
let D be finite set ; for f being Function of D,NAT ex h being FinSequence of D st
for d being Element of D holds card (Coim (h,d)) = f . d
for i being Nat holds S1[i]
from NAT_1:sch 2(A1, A4);
then
S1[ card D]
;
hence
for f being Function of D,NAT ex h being FinSequence of D st
for d being Element of D holds card (Coim (h,d)) = f . d
; verum