let C, D, E be non empty set ; for f being Function of [:C,D:],E ex g being Function of [:D,C:],E st
for d being Element of D
for c being Element of C holds g . (d,c) = f . (c,d)
let f be Function of [:C,D:],E; ex g being Function of [:D,C:],E st
for d being Element of D
for c being Element of C holds g . (d,c) = f . (c,d)
deffunc H1( Element of D, Element of C) -> Element of E = f . ($2,$1);
consider IT being Function of [:D,C:],E such that
A1:
for d being Element of D
for c being Element of C holds IT . (d,c) = H1(d,c)
from STACKS_1:sch 2();
take
IT
; for d being Element of D
for c being Element of C holds IT . (d,c) = f . (c,d)
thus
for d being Element of D
for c being Element of C holds IT . (d,c) = f . (c,d)
by A1; verum