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