set O = OwnSymbolsOf S;
set f = I | ();
set D = dom (I | ());
set C = U \/ BOOLEAN;
now :: thesis: for y being object st y in rng (I | ()) holds
y in PFuncs ((U *),())
let y be object ; :: thesis: ( y in rng (I | ()) implies y in PFuncs ((U *),()) )
assume y in rng (I | ()) ; :: thesis: y in PFuncs ((U *),())
then y in (I | ()) .: (dom (I | ())) ;
then consider x being object such that
A1: ( x in dom (I | ()) & x in dom (I | ()) & y = (I | ()) . x ) by FUNCT_1:def 6;
x in OwnSymbolsOf S by A1;
then reconsider s = x as own Element of S by FOMODEL1:def 19;
reconsider n = |.(ar s).| as Element of NAT ;
reconsider DD = n -tuples_on U as Subset of (U *) by FINSEQ_2:134;
U \/ BOOLEAN c= U \/ BOOLEAN ;
then reconsider CC = U \/ BOOLEAN as Subset of () ;
(I | ()) . x = I . s by ;
then reconsider g = (I | ()) . x as Function of DD,CC ;
[:DD,CC:] c= [:(U *),():] ;
then reconsider gg = g as Relation of (U *),() by XBOOLE_1:1;
gg is PartFunc of (U *),() ;
hence y in PFuncs ((U *),()) by ; :: thesis: verum
end;
hence for b1 being Function st b1 = I | () holds
b1 is PFuncs ((U *),()) -valued by ; :: thesis: verum