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 )
set ElofE = the Element of E;
deffunc H₁( object ) -> Element of E = the Element of E;
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:4;
deffunc H₂( object ) -> set = g . $1;
defpred S₁[ object ] means $1 in dom g;

A2: now :: thesis: for q being object st q in omega holds
( ( S₁[q] implies H₂(q) in E ) & ( not S₁[q] implies H₁(q) in E ) )

let q be object ; :: 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 :: thesis: ( q in dom g implies g . q in E )

assume q in dom g ; :: thesis: g . q in E
then g . q in rng g by FUNCT_1:def 3;
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 object 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:4;
then reconsider f = h * (decode ") as Function of VAR,E by FUNCT_2:13;
take f ; :: thesis: p = (f * decode) | fs
A4: dom h = omega by FUNCT_2:def 1;
then A5: dom g = (dom h) /\ fs by A1, XBOOLE_1:28;
A6: for p being object st p in dom g holds
h . p = g . p by A1, A3;
h = h * (id (dom decode)) by A4, Lm1, RELAT_1:51
.= h * ((decode ") * decode) by Lm1, FUNCT_1:39
.= f * decode by RELAT_1:36 ;
hence p = (f * decode) | fs by A5, A6, FUNCT_1:46; :: thesis: verum