let X be set ; :: thesis: for C, D being non empty set

for f being PartFunc of C,D st X meets dom f holds

( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} )

let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st X meets dom f holds

( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} )

let f be PartFunc of C,D; :: thesis: ( X meets dom f implies ( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} ) )

assume A1: X /\ (dom f) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: ( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} )

thus ( f | X is V8() implies ex d being Element of D st rng (f | X) = {d} ) :: thesis: ( ex d being Element of D st rng (f | X) = {d} implies f | X is V8() )

take d ; :: according to PARTFUN2:def 1 :: thesis: for c being Element of C st c in dom (f | X) holds

(f | X) . c = d

let c be Element of C; :: thesis: ( c in dom (f | X) implies (f | X) . c = d )

assume A8: c in dom (f | X) ; :: thesis: (f | X) . c = d

then (f | X) /. c in {d} by A7, Th2;

then (f | X) . c in {d} by A8, PARTFUN1:def 6;

hence (f | X) . c = d by TARSKI:def 1; :: thesis: verum

for f being PartFunc of C,D st X meets dom f holds

( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} )

let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st X meets dom f holds

( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} )

let f be PartFunc of C,D; :: thesis: ( X meets dom f implies ( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} ) )

assume A1: X /\ (dom f) <> {} ; :: according to XBOOLE_0:def 7 :: thesis: ( f | X is V8() iff ex d being Element of D st rng (f | X) = {d} )

thus ( f | X is V8() implies ex d being Element of D st rng (f | X) = {d} ) :: thesis: ( ex d being Element of D st rng (f | X) = {d} implies f | X is V8() )

proof

given d being Element of D such that A7:
rng (f | X) = {d}
; :: thesis: f | X is V8()
assume
f | X is V8()
; :: thesis: ex d being Element of D st rng (f | X) = {d}

then consider d being Element of D such that

A2: for c being Element of C st c in X /\ (dom f) holds

f /. c = d by Th35;

take d ; :: thesis: rng (f | X) = {d}

thus rng (f | X) c= {d} :: according to XBOOLE_0:def 10 :: thesis: {d} c= rng (f | X)

end;then consider d being Element of D such that

A2: for c being Element of C st c in X /\ (dom f) holds

f /. c = d by Th35;

take d ; :: thesis: rng (f | X) = {d}

thus rng (f | X) c= {d} :: according to XBOOLE_0:def 10 :: thesis: {d} c= rng (f | X)

proof

thus
{d} c= rng (f | X)
:: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (f | X) or x in {d} )

assume x in rng (f | X) ; :: thesis: x in {d}

then consider y being object such that

A3: y in dom (f | X) and

A4: (f | X) . y = x by FUNCT_1:def 3;

reconsider y = y as Element of C by A3;

dom (f | X) = X /\ (dom f) by RELAT_1:61;

then d = f /. y by A2, A3

.= (f | X) /. y by A3, Th15

.= x by A3, A4, PARTFUN1:def 6 ;

hence x in {d} by TARSKI:def 1; :: thesis: verum

end;assume x in rng (f | X) ; :: thesis: x in {d}

then consider y being object such that

A3: y in dom (f | X) and

A4: (f | X) . y = x by FUNCT_1:def 3;

reconsider y = y as Element of C by A3;

dom (f | X) = X /\ (dom f) by RELAT_1:61;

then d = f /. y by A2, A3

.= (f | X) /. y by A3, Th15

.= x by A3, A4, PARTFUN1:def 6 ;

hence x in {d} by TARSKI:def 1; :: thesis: verum

proof

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

the Element of X /\ (dom f) in dom f by A1, XBOOLE_0:def 4;

then reconsider y = the Element of X /\ (dom f) as Element of C ;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {d} or x in rng (f | X) )

assume A5: x in {d} ; :: thesis: x in rng (f | X)

A6: dom (f | X) = X /\ (dom f) by RELAT_1:61;

then (f | X) /. y = f /. y by A1, Th15

.= d by A1, A2

.= x by A5, TARSKI:def 1 ;

hence x in rng (f | X) by A1, A6, Th2; :: thesis: verum

end;the Element of X /\ (dom f) in dom f by A1, XBOOLE_0:def 4;

then reconsider y = the Element of X /\ (dom f) as Element of C ;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {d} or x in rng (f | X) )

assume A5: x in {d} ; :: thesis: x in rng (f | X)

A6: dom (f | X) = X /\ (dom f) by RELAT_1:61;

then (f | X) /. y = f /. y by A1, Th15

.= d by A1, A2

.= x by A5, TARSKI:def 1 ;

hence x in rng (f | X) by A1, A6, Th2; :: thesis: verum

take d ; :: according to PARTFUN2:def 1 :: thesis: for c being Element of C st c in dom (f | X) holds

(f | X) . c = d

let c be Element of C; :: thesis: ( c in dom (f | X) implies (f | X) . c = d )

assume A8: c in dom (f | X) ; :: thesis: (f | X) . c = d

then (f | X) /. c in {d} by A7, Th2;

then (f | X) . c in {d} by A8, PARTFUN1:def 6;

hence (f | X) . c = d by TARSKI:def 1; :: thesis: verum