let fs be finite Subset of omega; :: thesis: 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 )
let E be non empty set ; :: thesis: 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 )
let f be Function of VAR,E; :: thesis: ( dom ((f * decode) | fs) = fs & rng ((f * decode) | fs) c= E & (f * decode) | fs in Funcs (fs,E) & dom (f * decode) = omega )
dom (f * decode) = omega by FUNCT_2:def 1;
hence A1: dom ((f * decode) | fs) = fs by RELAT_1:62; :: thesis: ( rng ((f * decode) | fs) c= E & (f * decode) | fs in Funcs (fs,E) & dom (f * decode) = omega )
thus rng ((f * decode) | fs) c= E ; :: thesis: ( (f * decode) | fs in Funcs (fs,E) & dom (f * decode) = omega )
hence (f * decode) | fs in Funcs (fs,E) by A1, FUNCT_2:def 2; :: thesis: dom (f * decode) = omega
thus dom (f * decode) = omega by FUNCT_2:def 1; :: thesis: verum