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 object 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 object 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 object 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 object 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 object 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 object 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;
( rng F c= D1 & rng F c= D2 )
by A4;
then A5:
( F is D1 -valued & F is D2 -valued )
by RELAT_1:def 19;
then consider F1 being sequence of D1 such that
A6:
F1 . 0 = F . 0
and
A7:
for n being Nat st n + 1 < len F holds
F1 . (n + 1) = b1 . ((F1 . n),(F . (n + 1)))
and
A8:
b1 "**" F = F1 . ((len F) - 1)
by A1, Def8;
consider F2 being sequence of D2 such that
A9:
F2 . 0 = F . 0
and
A10:
for n being Nat st n + 1 < len F holds
F2 . (n + 1) = b2 . ((F2 . n),(F . (n + 1)))
and
A11:
b2 "**" F = F2 . ((len F) - 1)
by A1, Def8, A5;
defpred S1[ Nat] means ( $1 < len F implies ( F1 . $1 = F2 . $1 & F1 . $1 in D ) );
0 in dom F
by A1, AFINSQ_1:86;
then
F . 0 in rng F
by FUNCT_1:def 3;
then A12:
S1[ 0 ]
by A6, A9;
A13:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A14:
S1[
n]
;
S1[n + 1]
assume A15:
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, AFINSQ_1:86;
then A16:
(
F . (n + 1) in rng F &
n in dom F )
by FUNCT_1:def 3, AFINSQ_1:86;
A17:
F1 . (n + 1) = b1 . (
(F1 . n),
(F . (n + 1)))
by A7, A15;
then F1 . (n + 1) =
b2 . (
(F2 . n),
(F . (n + 1)))
by A3, A16, A14, AFINSQ_1:86
.=
F2 . (n + 1)
by A10, A15
;
hence
(
F1 . (n + 1) = F2 . (n + 1) &
F1 . (n + 1) in D )
by A16, A14, A17, A3, AFINSQ_1:86;
verum
end;
reconsider l1 = (len F) - 1 as Element of NAT by A1, NAT_1:21;
A18:
l1 < l1 + 1
by NAT_1:13;
for n being Nat holds S1[n]
from NAT_1:sch 2(A12, A13);
hence
b1 "**" F = b2 "**" F
by A8, A11, A18; verum