theorem :: ZF_FUND1:31

for fs being finite Subset of omega
for E being non empty set
for f being Function of VAR,E holds
( dom ((f * decode) | fs) = fs & rng ((f * decode) | fs) c= E & (f * decode) | fs in Funcs (fs,E) & dom (f * decode) = omega ) by Lm3;