let C, D, E be non empty set ; :: thesis: for c being Element of C

for e being Element of E

for f being PartFunc of C,D

for s being PartFunc of D,E st [c,e] in s * f holds

( [c,(f /. c)] in f & [(f /. c),e] in s )

let c be Element of C; :: thesis: for e being Element of E

for f being PartFunc of C,D

for s being PartFunc of D,E st [c,e] in s * f holds

( [c,(f /. c)] in f & [(f /. c),e] in s )

let e be Element of E; :: thesis: for f being PartFunc of C,D

for s being PartFunc of D,E st [c,e] in s * f holds

( [c,(f /. c)] in f & [(f /. c),e] in s )

let f be PartFunc of C,D; :: thesis: for s being PartFunc of D,E st [c,e] in s * f holds

( [c,(f /. c)] in f & [(f /. c),e] in s )

let s be PartFunc of D,E; :: thesis: ( [c,e] in s * f implies ( [c,(f /. c)] in f & [(f /. c),e] in s ) )

assume A1: [c,e] in s * f ; :: thesis: ( [c,(f /. c)] in f & [(f /. c),e] in s )

then A2: [(f . c),e] in s by GRFUNC_1:4;

A3: [c,(f . c)] in f by A1, GRFUNC_1:4;

then c in dom f by FUNCT_1:1;

hence ( [c,(f /. c)] in f & [(f /. c),e] in s ) by A3, A2, PARTFUN1:def 6; :: thesis: verum

for e being Element of E

for f being PartFunc of C,D

for s being PartFunc of D,E st [c,e] in s * f holds

( [c,(f /. c)] in f & [(f /. c),e] in s )

let c be Element of C; :: thesis: for e being Element of E

for f being PartFunc of C,D

for s being PartFunc of D,E st [c,e] in s * f holds

( [c,(f /. c)] in f & [(f /. c),e] in s )

let e be Element of E; :: thesis: for f being PartFunc of C,D

for s being PartFunc of D,E st [c,e] in s * f holds

( [c,(f /. c)] in f & [(f /. c),e] in s )

let f be PartFunc of C,D; :: thesis: for s being PartFunc of D,E st [c,e] in s * f holds

( [c,(f /. c)] in f & [(f /. c),e] in s )

let s be PartFunc of D,E; :: thesis: ( [c,e] in s * f implies ( [c,(f /. c)] in f & [(f /. c),e] in s ) )

assume A1: [c,e] in s * f ; :: thesis: ( [c,(f /. c)] in f & [(f /. c),e] in s )

then A2: [(f . c),e] in s by GRFUNC_1:4;

A3: [c,(f . c)] in f by A1, GRFUNC_1:4;

then c in dom f by FUNCT_1:1;

hence ( [c,(f /. c)] in f & [(f /. c),e] in s ) by A3, A2, PARTFUN1:def 6; :: thesis: verum