let C, D, E be non empty set ; :: thesis: 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; :: thesis: 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 H₁( 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) = H₁(d,c) from STACKS_1:sch 2();
take IT ; :: thesis: 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; :: thesis: verum