let f be Interpreter of s,U; :: thesis: f is Function of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN)
set n = abs (ar s);
set D = (abs (ar s)) -tuples_on U;
set C = U \/ BOOLEAN;
(abs (ar s)) -tuples_on U c= ((abs (ar s)) -tuples_on U) \/ {} ;
then reconsider DD = (abs (ar s)) -tuples_on U as Subset of ((abs (ar s)) -tuples_on U) ;
reconsider C1 = BOOLEAN , C2 = U as Subset of (U \/ BOOLEAN) by XBOOLE_1:7;

per cases ( s is relational or not s is relational ) ;

suppose s is relational ; :: thesis: f is Function of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN)

then reconsider ff = f as Function of DD,C1 by DefInterpreter1;
[:DD,C1:] c= [:((abs (ar s)) -tuples_on U),(U \/ BOOLEAN):] ;
then reconsider fff = ff as Relation of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN) by XBOOLE_1:1;
fff is Function of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN) ;
hence f is Function of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN) ; :: thesis: verum

end;

suppose not s is relational ; :: thesis: f is Function of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN)

then reconsider ff = f as Function of DD,C2 by DefInterpreter1;
[:DD,C2:] c= [:((abs (ar s)) -tuples_on U),(U \/ BOOLEAN):] ;
then reconsider fff = ff as Relation of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN) by XBOOLE_1:1;
fff is Function of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN) ;
hence f is Function of ((abs (ar s)) -tuples_on U),(U \/ BOOLEAN) ; :: thesis: verum

end;

end;