let X be set ; :: thesis: for C, D being non empty set
for f being PartFunc of C,D st X meets dom f holds
( f | X is constant iff ex d being Element of D st rng (f | X) = {d} )
let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st X meets dom f holds
( f | X is constant iff ex d being Element of D st rng (f | X) = {d} )
let f be PartFunc of C,D; :: thesis: ( X meets dom f implies ( f | X is constant iff ex d being Element of D st rng (f | X) = {d} ) )
assume A1: X /\ (dom f) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: ( f | X is constant iff ex d being Element of D st rng (f | X) = {d} )
thus ( f | X is constant implies ex d being Element of D st rng (f | X) = {d} ) :: thesis: ( ex d being Element of D st rng (f | X) = {d} implies f | X is constant )

proof

assume f | X is constant ; :: thesis: ex d being Element of D st rng (f | X) = {d}
then consider d being Element of D such that
A2: for c being Element of C st c in X /\ (dom f) holds
f /. c = d by Th54;
take d ; :: thesis: rng (f | X) = {d}
thus rng (f | X) c= {d} :: according to XBOOLE_0:def 10 :: thesis: {d} c= rng (f | X)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f | X) or x in {d} )
assume x in rng (f | X) ; :: thesis: x in {d}
then consider y being set such that
A3: y in dom (f | X) and
A4: (f | X) . y = x by FUNCT_1:def 3;
reconsider y = y as Element of C by A3;
dom (f | X) = X /\ (dom f) by RELAT_1:61;
then d = f /. y by A2, A3
.= (f | X) /. y by A3, Th32
.= x by A3, A4, PARTFUN1:def 6 ;
hence x in {d} by TARSKI:def 1; :: thesis: verum

end;

thus {d} c= rng (f | X) :: thesis: verum

proof

set y = the Element of X /\ (dom f);
the Element of X /\ (dom f) in dom f by A1, XBOOLE_0:def 4;
then reconsider y = the Element of X /\ (dom f) as Element of C ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {d} or x in rng (f | X) )
assume A5: x in {d} ; :: thesis: x in rng (f | X)
A6: dom (f | X) = X /\ (dom f) by RELAT_1:61;
then (f | X) /. y = f /. y by A1, Th32
.= d by A1, A2
.= x by A5, TARSKI:def 1 ;
hence x in rng (f | X) by A1, A6, Th4; :: thesis: verum

end;

end;

given d being Element of D such that A7: rng (f | X) = {d} ; :: thesis: f | X is constant
take d ; :: according to PARTFUN2:def 1 :: thesis: for c being Element of C st c in dom (f | X) holds
(f | X) . c = d
let c be Element of C; :: thesis: ( c in dom (f | X) implies (f | X) . c = d )
assume A8: c in dom (f | X) ; :: thesis: (f | X) . c = d
then (f | X) /. c in {d} by A7, Th4;
then (f | X) . c in {d} by A8, PARTFUN1:def 6;
hence (f | X) . c = d by TARSKI:def 1; :: thesis: verum