let D be non empty set ; for F being XFinSequence of D
for D1, D2 being non empty set
for b1 being BinOp of D1
for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds
b1 "**" F = b2 "**" F
let F be XFinSequence of D; for D1, D2 being non empty set
for b1 being BinOp of D1
for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds
b1 "**" F = b2 "**" F
let D1, D2 be non empty set ; for b1 being BinOp of D1
for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds
b1 "**" F = b2 "**" F
let b1 be BinOp of D1; for b2 being BinOp of D2 st len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) holds
b1 "**" F = b2 "**" F
let b2 be BinOp of D2; ( len F >= 1 & D c= D1 /\ D2 & ( for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D ) ) implies b1 "**" F = b2 "**" F )
assume that
A1:
len F >= 1
and
A2:
D c= D1 /\ D2
and
A3:
for x, y being set st x in D & y in D holds
( b1 . (x,y) = b2 . (x,y) & b1 . (x,y) in D )
; b1 "**" F = b2 "**" F
( D1 /\ D2 c= D1 & D1 /\ D2 c= D2 )
by XBOOLE_1:17;
then A4:
( D c= D1 & D c= D2 )
by A2, XBOOLE_1:1;
A5:
rng F c= D
by RELAT_1:def 19;
then
( rng F c= D1 & rng F c= D2 )
by A4, XBOOLE_1:1;
then A6:
( F is D1 -valued & F is D2 -valued )
by RELAT_1:def 19;
then consider F1 being Function of NAT,D1 such that
A7:
F1 . 0 = F . 0
and
A8:
for n being Nat st n + 1 < len F holds
F1 . (n + 1) = b1 . ((F1 . n),(F . (n + 1)))
and
A9:
b1 "**" F = F1 . ((len F) - 1)
by A1, Def9;
consider F2 being Function of NAT,D2 such that
A10:
F2 . 0 = F . 0
and
A11:
for n being Nat st n + 1 < len F holds
F2 . (n + 1) = b2 . ((F2 . n),(F . (n + 1)))
and
A12:
b2 "**" F = F2 . ((len F) - 1)
by A1, Def9, A6;
defpred S1[ Nat] means ( $1 < len F implies ( F1 . $1 = F2 . $1 & F1 . $1 in D ) );
0 in dom F
by A1, NAT_1:44;
then
F . 0 in rng F
by FUNCT_1:def 3;
then A13:
S1[ 0 ]
by A5, A7, A10;
A14:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A15:
S1[
n]
;
S1[n + 1]
assume A16:
n + 1
< len F
;
( F1 . (n + 1) = F2 . (n + 1) & F1 . (n + 1) in D )
then
(
n + 1
in dom F &
n < len F )
by NAT_1:13, NAT_1:44;
then A17:
(
F . (n + 1) in rng F &
n in dom F )
by FUNCT_1:def 3, NAT_1:44;
A18:
F1 . (n + 1) = b1 . (
(F1 . n),
(F . (n + 1)))
by A8, A16;
then F1 . (n + 1) =
b2 . (
(F2 . n),
(F . (n + 1)))
by A3, A5, A17, A15, NAT_1:44
.=
F2 . (n + 1)
by A11, A16
;
hence
(
F1 . (n + 1) = F2 . (n + 1) &
F1 . (n + 1) in D )
by A5, A17, A15, A18, A3, NAT_1:44;
verum
end;
reconsider l1 = (len F) - 1 as Element of NAT by A1, NAT_1:21;
A19:
l1 < l1 + 1
by NAT_1:13;
for n being Nat holds S1[n]
from NAT_1:sch 2(A13, A14);
hence
b1 "**" F = b2 "**" F
by A9, A12, A19; verum