let p be set ; :: thesis: for fs being finite Subset of omega
for E being non empty set st p in Funcs fs,E holds
ex f being Function of VAR ,E st p = (f * decode ) | fs
let fs be finite Subset of omega ; :: thesis: for E being non empty set st p in Funcs fs,E holds
ex f being Function of VAR ,E st p = (f * decode ) | fs
let E be non empty set ; :: thesis: ( p in Funcs fs,E implies ex f being Function of VAR ,E st p = (f * decode ) | fs )
assume p in Funcs fs,E ; :: thesis: ex f being Function of VAR ,E st p = (f * decode ) | fs
then A1: ex e being Function st
( e = p & dom e = fs & rng e c= E ) by FUNCT_2:def 2;
then reconsider g = p as Function of fs,E by FUNCT_2:def 1, RELSET_1:11;
consider ElofE being Element of E;
defpred S₁[ set ] means $1 in dom g;
deffunc H₁( set ) -> set = g . $1;
deffunc H₂( set ) -> Element of E = ElofE;

A2: now

let q be set ; :: thesis: ( q in omega implies ( ( S₁[q] implies H₁(q) in E ) & ( not S₁[q] implies H₂(q) in E ) ) )
assume q in omega ; :: thesis: ( ( S₁[q] implies H₁(q) in E ) & ( not S₁[q] implies H₂(q) in E ) )

now

assume q in dom g ; :: thesis: g . q in E
then g . q in rng g by FUNCT_1:def 5;
hence g . q in E ; :: thesis: verum

end;

hence ( ( S₁[q] implies H₁(q) in E ) & ( not S₁[q] implies H₂(q) in E ) ) ; :: thesis: verum

end;

consider h being Function of omega ,E such that
A3: for q being set st q in omega holds
( ( S₁[q] implies h . q = H₁(q) ) & ( not S₁[q] implies h . q = H₂(q) ) ) from FUNCT_2:sch 5(A2);
decode " is Function of VAR ,omega by Lm1, FUNCT_2:def 1, RELSET_1:11;
then reconsider f = h * (decode " ) as Function of VAR ,E by FUNCT_2:19;
take f ; :: thesis: p = (f * decode ) | fs
A4: dom h = omega by FUNCT_2:def 1;
then A5: h = h * (id (dom decode )) by Lm1, RELAT_1:77
.= h * ((decode " ) * decode ) by Lm1, FUNCT_1:61
.= f * decode by RELAT_1:55 ;
g = h | fs

proof

A6: dom g = (dom h) /\ fs by A1, A4, XBOOLE_1:28;
for p being set st p in dom g holds
h . p = g . p by A1, A3;
hence g = h | fs by A6, FUNCT_1:68; :: thesis: verum

end;

hence p = (f * decode ) | fs by A5; :: thesis: verum