let X be set ; :: thesis: for C, D being non empty set
for f being PartFunc of C,D holds
( f | X is constant iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 )
let C, D be non empty set ; :: thesis: for f being PartFunc of C,D holds
( f | X is constant iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 )
let f be PartFunc of C,D; :: thesis: ( f | X is constant iff for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 )
thus ( f | X is constant implies for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 ) :: thesis: ( ( for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 ) implies f | X is constant )

proof

assume f | X is constant ; :: thesis: for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2
then consider d being Element of D such that
A1: for c being Element of C st c in X /\ (dom f) holds
f . c = d by Th57;
let c1, c2 be Element of C; :: thesis: ( c1 in X /\ (dom f) & c2 in X /\ (dom f) implies f . c1 = f . c2 )
assume that
A2: c1 in X /\ (dom f) and
A3: c2 in X /\ (dom f) ; :: thesis: f . c1 = f . c2
f . c1 = d by A1, A2;
hence f . c1 = f . c2 by A1, A3; :: thesis: verum

end;

assume A4: for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
f . c1 = f . c2 ; :: thesis: f | X is constant

now :: thesis: f | X is constant

per cases ( X /\ (dom f) = {} or X /\ (dom f) <> {} ) ;

suppose A5: X /\ (dom f) = {} ; :: thesis: f | X is constant

now :: thesis: ex d being Element of D st
for c being Element of C st c in X /\ (dom f) holds
f . c = d

set d = the Element of D;
take d = the Element of D; :: thesis: for c being Element of C st c in X /\ (dom f) holds
f . c = d
let c be Element of C; :: thesis: ( c in X /\ (dom f) implies f . c = d )
thus ( c in X /\ (dom f) implies f . c = d ) by A5; :: thesis: verum

end;

hence f | X is constant by Th57; :: thesis: verum

end;

suppose A6: X /\ (dom f) <> {} ; :: thesis: f | X is constant

set x = the Element of X /\ (dom f);

now :: thesis: for c being Element of C st c in X /\ (dom f) holds
f . c = f /. the Element of X /\ (dom f)

let c be Element of C; :: thesis: ( c in X /\ (dom f) implies f . c = f /. the Element of X /\ (dom f) )
A7: the Element of X /\ (dom f) in dom f by A6, XBOOLE_0:def 4;
assume c in X /\ (dom f) ; :: thesis: f . c = f /. the Element of X /\ (dom f)
hence f . c = f . the Element of X /\ (dom f) by A4, A7
.= f /. the Element of X /\ (dom f) by A7, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence f | X is constant by Th57; :: thesis: verum

end;

end;

end;

hence f | X is constant ; :: thesis: verum