set O = OwnSymbolsOf S;

set f = I | (OwnSymbolsOf S);

set D = dom (I | (OwnSymbolsOf S));

set C = U \/ BOOLEAN;

_{1} being Function st b_{1} = I | (OwnSymbolsOf S) holds

b_{1} is PFuncs ((U *),(U \/ BOOLEAN)) -valued
by RELAT_1:def 19, TARSKI:def 3; :: thesis: verum

set f = I | (OwnSymbolsOf S);

set D = dom (I | (OwnSymbolsOf S));

set C = U \/ BOOLEAN;

now :: thesis: for y being object st y in rng (I | (OwnSymbolsOf S)) holds

y in PFuncs ((U *),(U \/ BOOLEAN))

hence
for by in PFuncs ((U *),(U \/ BOOLEAN))

let y be object ; :: 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))) ;

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; :: thesis: verum

end;assume y in rng (I | (OwnSymbolsOf S)) ; :: thesis: 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; :: thesis: verum

b