let f be Interpreter of s,U; :: thesis: f is Function of (|.(ar s).| -tuples_on U),(U \/ BOOLEAN)
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 (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 (|.(ar s).| -tuples_on U),(U \/ BOOLEAN)

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

end;

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

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

end;

end;