let X be set ; :: thesis: for P being Relation st not X is empty & X is trivial & P is X -valued holds
P is constant Function
let P be Relation; :: thesis: ( not X is empty & X is trivial & P is X -valued implies P is constant Function )
assume ( not X is empty & X is trivial ) ; :: thesis: ( not P is X -valued or P is constant Function )
then reconsider T = X as non empty trivial set ;
consider t being Element of T such that
A1: T = {t} by SUBSET_1:46;
set d = dom P;
set r = rng P;
reconsider f = [:(dom P),{t}:] as Function ;
assume P is X -valued ; :: thesis: P is constant Function
then reconsider r = rng P as Subset of {t} by A1;
[:(dom P),r:] \ [:((dom P) \/ {}),({t} null r):] = {} ;
then ( P c= [:(dom P),r:] & [:(dom P),r:] c= f ) by RELAT_1:7, Th29;
then reconsider fP = P as Function-like Subset of f by XBOOLE_1:1;
( (rng fP) \ (rng f) = {} & (rng f) \ {t} = {} ) ;
then ( rng fP c= rng f & rng f c= {t} ) by Th29;
hence P is constant Function ; :: thesis: verum