let X be set ; :: thesis: for C, D being non empty set
for f being PartFunc of C,D holds
( f | X is V8() 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 V8() 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 V8() 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 V8() 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 V8() )
proof
assume f | X is V8() ; :: 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 Th35;
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 V8()
now :: thesis: f | X is V8()
per cases ( X /\ (dom f) = {} or X /\ (dom f) <> {} ) ;
suppose A5: X /\ (dom f) = {} ; :: thesis: f | X is V8()
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 V8() by Th35; :: thesis: verum
end;
suppose A6: X /\ (dom f) <> {} ; :: thesis: f | X is V8()
set x = the Element of X /\ (dom f);
the Element of X /\ (dom f) in dom f by ;
then reconsider x = the Element of X /\ (dom f) as Element of C ;
for c being Element of C st c in X /\ (dom f) holds
f /. c = f /. x by A4;
hence f | X is V8() by Th35; :: thesis: verum
end;
end;
end;
hence f | X is V8() ; :: thesis: verum