let D be non empty set ; :: thesis: for I, J being non empty set
for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ X,((curry' f) . j) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ [:X,Y:],f = F $$ Y,g
let I, J be non empty set ; :: thesis: for F being BinOp of D
for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ X,((curry' f) . j) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ [:X,Y:],f = F $$ Y,g
let F be BinOp of D; :: thesis: for f being Function of [:I,J:],D
for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ X,((curry' f) . j) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ [:X,Y:],f = F $$ Y,g
let f be Function of [:I,J:],D; :: thesis: for g being Function of J,D
for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ X,((curry' f) . j) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ [:X,Y:],f = F $$ Y,g
let g be Function of J,D; :: thesis: for X being Element of Fin I
for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ X,((curry' f) . j) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ [:X,Y:],f = F $$ Y,g
let X be Element of Fin I; :: thesis: for Y being Element of Fin J st ( for j being Element of J holds g . j = F $$ X,((curry' f) . j) ) & F is having_a_unity & F is commutative & F is associative holds
F $$ [:X,Y:],f = F $$ Y,g
let Y be Element of Fin J; :: thesis: ( ( for j being Element of J holds g . j = F $$ X,((curry' f) . j) ) & F is having_a_unity & F is commutative & F is associative implies F $$ [:X,Y:],f = F $$ Y,g )
assume that
A1: for j being Element of J holds g . j = F $$ X,((curry' f) . j) and
A2: ( F is having_a_unity & F is commutative & F is associative ) ; :: thesis: F $$ [:X,Y:],f = F $$ Y,g
defpred S₁[ Element of Fin J] means F $$ [:X,$1:],f = F $$ $1,g;
A3: for Y1 being Element of Fin J
for y being Element of J st S₁[Y1] holds
S₁[Y1 \/ {.y.}]

proof

let Y1 be Element of Fin J; :: thesis: for y being Element of J st S₁[Y1] holds
S₁[Y1 \/ {.y.}]
let y be Element of J; :: thesis: ( S₁[Y1] implies S₁[Y1 \/ {.y.}] )
assume A4: F $$ [:X,Y1:],f = F $$ Y1,g ; :: thesis: S₁[Y1 \/ {.y.}]
reconsider s = {.y.} as Element of Fin J ;

per cases ( y in Y1 or not y in Y1 ) ;

suppose y in Y1 ; :: thesis: S₁[Y1 \/ {.y.}]

then Y1 \/ {y} = Y1 by ZFMISC_1:46;
hence S₁[Y1 \/ {.y.}] by A4; :: thesis: verum

end;

suppose not y in Y1 ; :: thesis: S₁[Y1 \/ {.y.}]

then A5: Y1 misses {y} by ZFMISC_1:56;
then A6: [:X,Y1:] misses [:X,s:] by ZFMISC_1:127;
thus F $$ [:X,(Y1 \/ {.y.}):],f = F $$ ([:X,Y1:] \/ [:X,s:]),f by ZFMISC_1:120
.= F . (F $$ [:X,Y1:],f),(F $$ [:X,s:],f) by A2, A6, SETWOP_2:6
.= F . (F $$ Y1,g),(F $$ s,g) by A1, A2, A4, Th33
.= F $$ (Y1 \/ {.y.}),g by A2, A5, SETWOP_2:6 ; :: thesis: verum

end;

end;

end;

A7: S₁[ {}. J]

proof

reconsider T = {}. [:I,J:] as Element of Fin [:I,J:] ;
T = [:X,({}. J):] by ZFMISC_1:113;
then F $$ [:X,({}. J):],f = the_unity_wrt F by A2, SETWISEO:40;
hence S₁[ {}. J] by A2, SETWISEO:40; :: thesis: verum

end;

for Y1 being Element of Fin J holds S₁[Y1] from SETWISEO:sch 4(A7, A3);
hence F $$ [:X,Y:],f = F $$ Y,g ; :: thesis: verum