theorem T2103: :: FINSEQ_9:16

for C being set
for f being b₁ -defined total Function holds f is Function of C,(rng f)