let f be Interpreter of s,U; :: thesis: f is Function of (|.(ar s).| -tuples_on U),()
set n = |.(ar s).|;
set D = |.(ar s).| -tuples_on U;
set C = U \/ BOOLEAN;
|.(ar s).| -tuples_on U c= (|.(ar s).| -tuples_on U) \/ {} ;
then reconsider DD = |.(ar s).| -tuples_on U as Subset of (|.(ar s).| -tuples_on U) ;
reconsider C1 = BOOLEAN , C2 = U as Subset of () by XBOOLE_1:7;
per cases ( s is relational or not s is relational ) ;
suppose s is relational ; :: thesis: f is Function of (|.(ar s).| -tuples_on U),()
then reconsider ff = f as Function of DD,C1 by Def2;
[:DD,C1:] c= [:(|.(ar s).| -tuples_on U),():] ;
then reconsider fff = ff as Relation of (|.(ar s).| -tuples_on U),() by XBOOLE_1:1;
fff is Function of (|.(ar s).| -tuples_on U),() ;
hence f is Function of (|.(ar s).| -tuples_on U),() ; :: thesis: verum
end;
suppose not s is relational ; :: thesis: f is Function of (|.(ar s).| -tuples_on U),()
then reconsider ff = f as Function of DD,C2 by Def2;
[:DD,C2:] c= [:(|.(ar s).| -tuples_on U),():] ;
then reconsider fff = ff as Relation of (|.(ar s).| -tuples_on U),() by XBOOLE_1:1;
fff is Function of (|.(ar s).| -tuples_on U),() ;
hence f is Function of (|.(ar s).| -tuples_on U),() ; :: thesis: verum
end;
end;