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() )

f /. c1 = f /. c2 ; :: thesis: f | X is V8()

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 A4:
for c1, c2 being Element of C st c1 in X /\ (dom f) & c2 in X /\ (dom f) holds
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;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

f /. c1 = f /. c2 ; :: thesis: f | X is V8()

now :: thesis: f | X is V8()end;

hence
f | X is V8()
; :: thesis: verumper cases
( X /\ (dom f) = {} or X /\ (dom f) <> {} )
;

end;

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

end;

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

hence
f | X is V8()
by Th35; :: thesis: verumfor 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;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

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 A6, XBOOLE_0:def 4;

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;the Element of X /\ (dom f) in dom f by A6, XBOOLE_0:def 4;

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