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 [c,e] in s * f ; :: thesis: ( [c,(f /. c)] in f & [(f /. c),e] in s )
then A1: ( [c,(f . c)] in f & [(f . c),e] in s ) by GRFUNC_1:12;
then c in dom f by FUNCT_1:8;
hence ( [c,(f /. c)] in f & [(f /. c),e] in s ) by A1, PARTFUN1:def 8; :: thesis: verum