let X1, X2, Y be non empty set ; :: thesis: for F being BinOp of Y
for B1 being Element of Fin X1
for B2 being Element of Fin X2 st B1 = B2 & ( B1 <> {} or F is having_a_unity ) & F is associative & F is commutative holds
for f1 being Function of X1,Y
for f2 being Function of X2,Y st f1 | B1 = f2 | B2 holds
F $$ (B1,f1) = F $$ (B2,f2)
let F be BinOp of Y; :: thesis: for B1 being Element of Fin X1
for B2 being Element of Fin X2 st B1 = B2 & ( B1 <> {} or F is having_a_unity ) & F is associative & F is commutative holds
for f1 being Function of X1,Y
for f2 being Function of X2,Y st f1 | B1 = f2 | B2 holds
F $$ (B1,f1) = F $$ (B2,f2)
let B1 be Element of Fin X1; :: thesis: for B2 being Element of Fin X2 st B1 = B2 & ( B1 <> {} or F is having_a_unity ) & F is associative & F is commutative holds
for f1 being Function of X1,Y
for f2 being Function of X2,Y st f1 | B1 = f2 | B2 holds
F $$ (B1,f1) = F $$ (B2,f2)
let B2 be Element of Fin X2; :: thesis: ( B1 = B2 & ( B1 <> {} or F is having_a_unity ) & F is associative & F is commutative implies for f1 being Function of X1,Y
for f2 being Function of X2,Y st f1 | B1 = f2 | B2 holds
F $$ (B1,f1) = F $$ (B2,f2) )
assume that
A1: B1 = B2 and
A2: ( ( B1 <> {} or F is having_a_unity ) & F is associative & F is commutative ) ; :: thesis: for f1 being Function of X1,Y
for f2 being Function of X2,Y st f1 | B1 = f2 | B2 holds
F $$ (B1,f1) = F $$ (B2,f2)
let f1 be Function of X1,Y; :: thesis: for f2 being Function of X2,Y st f1 | B1 = f2 | B2 holds
F $$ (B1,f1) = F $$ (B2,f2)
let f2 be Function of X2,Y; :: thesis: ( f1 | B1 = f2 | B2 implies F $$ (B1,f1) = F $$ (B2,f2) )
assume A3: f1 | B1 = f2 | B2 ; :: thesis: F $$ (B1,f1) = F $$ (B2,f2)
consider G1 being Function of (Fin X1),Y such that
A4: F $$ (B1,f1) = G1 . B1 and
A5: for e being Element of Y st e is_a_unity_wrt F holds
G1 . {} = e and
A6: for x being Element of X1 holds G1 . {x} = f1 . x and
A7: for B9 being Element of Fin X1 st B9 c= B1 & B9 <> {} holds
for x being Element of X1 st x in B1 \ B9 holds
G1 . (B9 \/ {x}) = F . ((G1 . B9),(f1 . x)) by A2, SETWISEO:def 3;
consider G2 being Function of (Fin X2),Y such that
A8: F $$ (B2,f2) = G2 . B2 and
A9: for e being Element of Y st e is_a_unity_wrt F holds
G2 . {} = e and
A10: for x being Element of X2 holds G2 . {x} = f2 . x and
A11: for B9 being Element of Fin X2 st B9 c= B2 & B9 <> {} holds
for x being Element of X2 st x in B2 \ B9 holds
G2 . (B9 \/ {x}) = F . ((G2 . B9),(f2 . x)) by A1, A2, SETWISEO:def 3;
defpred S₁[ set ] means ( not $1 c= B1 or G1 . $1 = G2 . $1 or $1 = {} );
A12: S₁[ {}. X1] ;
A13: for B9 being Element of Fin X1
for b being Element of X1 st S₁[B9] & not b in B9 holds
S₁[B9 \/ {b}]

proof

let B9 be Element of Fin X1; :: thesis: for b being Element of X1 st S₁[B9] & not b in B9 holds
S₁[B9 \/ {b}]
let b be Element of X1; :: thesis: ( S₁[B9] & not b in B9 implies S₁[B9 \/ {b}] )
assume A14: ( S₁[B9] & not b in B9 ) ; :: thesis: S₁[B9 \/ {b}]
assume A15: B9 \/ {b} c= B1 ; :: thesis: ( G1 . (B9 \/ {b}) = G2 . (B9 \/ {b}) or B9 \/ {b} = {} )
b in {b} by TARSKI:def 1;
then A16: b in B9 \/ {b} by XBOOLE_0:def 3;
then A17: b in B1 by A15;
A18: ( f1 . b = (f1 | B1) . b & f2 . b = (f2 | B2) . b ) by A1, A16, A15, FUNCT_1:49;
A19: B2 c= X2 by FINSUB_1:def 5;

per cases ( B9 = {} or B9 <> {} ) ;

suppose A20: B9 = {} ; :: thesis: ( G1 . (B9 \/ {b}) = G2 . (B9 \/ {b}) or B9 \/ {b} = {} )

( G1 . {b} = f1 . b & f1 . b = G2 . {b} ) by A6, A10, A3, A18, A19, A17, A1;
hence ( G1 . (B9 \/ {b}) = G2 . (B9 \/ {b}) or B9 \/ {b} = {} ) by A20; :: thesis: verum

end;

suppose A21: B9 <> {} ; :: thesis: ( G1 . (B9 \/ {b}) = G2 . (B9 \/ {b}) or B9 \/ {b} = {} )

A22: B9 c= B9 \/ {b} by XBOOLE_1:7;
then A23: B9 c= B1 by A15;
B9 c= X2 by A19, A1, A22, A15;
then reconsider B92 = B9 as Element of Fin X2 by FINSUB_1:def 5;
b in B1 \ B9 by A14, A16, A15, XBOOLE_0:def 5;
then ( G2 . (B92 \/ {b}) = F . ((G2 . B92),(f2 . b)) & G1 . (B9 \/ {b}) = F . ((G1 . B9),(f1 . b)) ) by A11, A7, A1, A21, A23, A19, A17;
hence ( G1 . (B9 \/ {b}) = G2 . (B9 \/ {b}) or B9 \/ {b} = {} ) by A18, A3, A23, A21, A14; :: thesis: verum

end;

end;

end;

A24: for B being Element of Fin X1 holds S₁[B] from SETWISEO:sch 2(A12, A13);

per cases ( B1 = {} or B1 <> {} ) ;

suppose A25: B1 = {} ; :: thesis: F $$ (B1,f1) = F $$ (B2,f2)

then ( G1 . {} = the_unity_wrt F & G2 . {} = the_unity_wrt F ) by A5, A9, A2, SETWISEO:14;
hence F $$ (B1,f1) = F $$ (B2,f2) by A4, A8, A25, A1; :: thesis: verum

end;

suppose B1 <> {} ; :: thesis: F $$ (B1,f1) = F $$ (B2,f2)

hence F $$ (B1,f1) = F $$ (B2,f2) by A24, A1, A4, A8; :: thesis: verum

end;

end;