set O = OwnSymbolsOf S;
set f = I | (OwnSymbolsOf S);
set D = dom (I | (OwnSymbolsOf S));
set C = U \/ BOOLEAN;
now for y being object st y in rng (I | (OwnSymbolsOf S)) holds
y in PFuncs ((U *),(U \/ BOOLEAN))let y be
object ;
( y in rng (I | (OwnSymbolsOf S)) implies y in PFuncs ((U *),(U \/ BOOLEAN)) )assume
y in rng (I | (OwnSymbolsOf S))
;
y in PFuncs ((U *),(U \/ BOOLEAN))then
y in (I | (OwnSymbolsOf S)) .: (dom (I | (OwnSymbolsOf S)))
;
then consider x being
object such that A1:
(
x in dom (I | (OwnSymbolsOf S)) &
x in dom (I | (OwnSymbolsOf S)) &
y = (I | (OwnSymbolsOf S)) . 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
(U \/ BOOLEAN) ;
(I | (OwnSymbolsOf S)) . x = I . s
by FUNCT_1:49, A1;
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 PARTFUN1:45, A1;
verum end;
hence
for b1 being Function st b1 = I | (OwnSymbolsOf S) holds
b1 is PFuncs ((U *),(U \/ BOOLEAN)) -valued
by RELAT_1:def 19, TARSKI:def 3; verum