set O = OwnSymbolsOf S;
set f = I | (OwnSymbolsOf S);
set D = dom (I | (OwnSymbolsOf S));
set C = U \/ BOOLEAN;

now

let y be set ; :: thesis: ( y in rng (I | (OwnSymbolsOf S)) implies y in PFuncs ((U *),(U \/ BOOLEAN)) )
assume y in rng (I | (OwnSymbolsOf S)) ; :: thesis: y in PFuncs ((U *),(U \/ BOOLEAN))
then y in (I | (OwnSymbolsOf S)) .: (dom (I | (OwnSymbolsOf S))) by RELAT_1:113;
then consider x being set such that
C1: ( x in dom (I | (OwnSymbolsOf S)) & x in dom (I | (OwnSymbolsOf S)) & y = (I | (OwnSymbolsOf S)) . x ) by FUNCT_1:def 6;
Z0: dom (I | (OwnSymbolsOf S)) c= OwnSymbolsOf S by RELAT_1:def 18;
then x in OwnSymbolsOf S by C1;
then reconsider s = x as own Element of S by FOMODEL1:def 19;
reconsider n = abs (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 (U \/ BOOLEAN) ;
(I | (OwnSymbolsOf S)) . x = I . s by C1, Z0, FUNCT_1:49;
then reconsider g = (I | (OwnSymbolsOf S)) . x as Function of DD,CC ;
[:DD,CC:] c= [:(U *),(U \/ BOOLEAN):] ;
then reconsider gg = g as Relation of (U *),(U \/ BOOLEAN) by XBOOLE_1:1;
gg is PartFunc of (U *),(U \/ BOOLEAN) ;
hence y in PFuncs ((U *),(U \/ BOOLEAN)) by C1, PARTFUN1:45; :: thesis: verum

end;

then rng (I | (OwnSymbolsOf S)) c= PFuncs ((U *),(U \/ BOOLEAN)) by TARSKI:def 3;
hence for b₁ being Function st b₁ = I | (OwnSymbolsOf S) holds
b₁ is PFuncs ((U *),(U \/ BOOLEAN)) -valued by RELAT_1:def 19; :: thesis: verum