let C, D, E be non empty set ; 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; 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; 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; 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; ( [c,e] in s * f implies ( [c,(f /. c)] in f & [(f /. c),e] in s ) )
assume A1:
[c,e] in s * f
; ( [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; verum