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

for f being PartFunc of C,D st f | X is V8() & Y c= X holds

f | Y is V8()

let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st f | X is V8() & Y c= X holds

f | Y is V8()

let f be PartFunc of C,D; :: thesis: ( f | X is V8() & Y c= X implies f | Y is V8() )

assume that

A1: f | X is V8() and

A2: Y c= X ; :: thesis: f | Y is V8()

consider d being Element of D such that

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

f /. c = d by A1, Th35;

for f being PartFunc of C,D st f | X is V8() & Y c= X holds

f | Y is V8()

let C, D be non empty set ; :: thesis: for f being PartFunc of C,D st f | X is V8() & Y c= X holds

f | Y is V8()

let f be PartFunc of C,D; :: thesis: ( f | X is V8() & Y c= X implies f | Y is V8() )

assume that

A1: f | X is V8() and

A2: Y c= X ; :: thesis: f | Y is V8()

consider d being Element of D such that

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

f /. c = d by A1, Th35;

now :: thesis: for c being Element of C st c in Y /\ (dom f) holds

f /. c = d

hence
f | Y is V8()
by Th35; :: thesis: verumf /. c = d

let c be Element of C; :: thesis: ( c in Y /\ (dom f) implies f /. c = d )

assume c in Y /\ (dom f) ; :: thesis: f /. c = d

then ( c in Y & c in dom f ) by XBOOLE_0:def 4;

then c in X /\ (dom f) by A2, XBOOLE_0:def 4;

hence f /. c = d by A3; :: thesis: verum

end;assume c in Y /\ (dom f) ; :: thesis: f /. c = d

then ( c in Y & c in dom f ) by XBOOLE_0:def 4;

then c in X /\ (dom f) by A2, XBOOLE_0:def 4;

hence f /. c = d by A3; :: thesis: verum