let X be set ; :: thesis: for D, C 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 D, C 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 Th76;
let c1, c2 be Element of C; :: thesis: ( c1 in X /\ (dom f) & c2 in X /\ (dom f) implies f . c1 = f . c2 )
assume ( c1 in X /\ (dom f) & c2 in X /\ (dom f) ) ; :: thesis: f . c1 = f . c2
then ( f . c1 = d & f . c2 = d ) by A1;
hence f . c1 = f . c2 ; :: thesis: verum

end;

assume A2: 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

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

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

now

consider d being Element of D;
take d = 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 A3; :: thesis: verum

end;

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

end;

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

consider x being Element of X /\ (dom f);

now

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

end;

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

end;

end;

end;

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