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:91; :: 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