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 I,D
for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) & F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp holds
F $$ [:X,Y:],f = F $$ X,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 I,D
for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) & F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp holds
F $$ [:X,Y:],f = F $$ X,g
let F be BinOp of D; :: thesis: for f being Function of [:I,J:],D
for g being Function of I,D
for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) & F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp holds
F $$ [:X,Y:],f = F $$ X,g
let f be Function of [:I,J:],D; :: thesis: for g being Function of I,D
for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) & F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp holds
F $$ [:X,Y:],f = F $$ X,g
let g be Function of I,D; :: thesis: for X being Element of Fin I
for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) & F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp holds
F $$ [:X,Y:],f = F $$ X,g
let X be Element of Fin I; :: thesis: for Y being Element of Fin J st ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) & F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp holds
F $$ [:X,Y:],f = F $$ X,g
let Y be Element of Fin J; :: thesis: ( ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) & F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp implies F $$ [:X,Y:],f = F $$ X,g )
assume A1: ( ( for i being Element of I holds g . i = F $$ Y,((curry f) . i) ) & F is having_a_unity & F is commutative & F is associative & F is having_an_inverseOp ) ; :: thesis: F $$ [:X,Y:],f = F $$ X,g
defpred S₁[ Element of Fin I] means F $$ [:$1,Y:],f = F $$ $1,g;
A2: S₁[ {}. I]

proof

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

end;

A3: for X1 being Element of Fin I
for x being Element of I st S₁[X1] holds
S₁[X1 \/ {.x.}]

proof

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

per cases ( x in X1 or not x in X1 ) ;

suppose x in X1 ; :: thesis: S₁[X1 \/ {.x.}]

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

end;

suppose not x in X1 ; :: thesis: S₁[X1 \/ {.x.}]

then A5: X1 misses {x} by ZFMISC_1:56;
then A6: [:X1,Y:] misses [:s,Y:] by ZFMISC_1:127;
thus F $$ [:(X1 \/ {.x.}),Y:],f = F $$ ([:X1,Y:] \/ [:s,Y:]),f by ZFMISC_1:120
.= F . (F $$ [:X1,Y:],f),(F $$ [:s,Y:],f) by A1, A6, SETWOP_2:6
.= F . (F $$ X1,g),(F $$ s,g) by A1, A4, Th31
.= F $$ (X1 \/ {.x.}),g by A1, A5, SETWOP_2:6 ; :: thesis: verum

end;

end;

end;

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