let X be set ; 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 ; 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; ( 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 )
( ( 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() )
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
; f | X is V8()
hence
f | X is V8()
; verum