let D be non empty set ; :: thesis: for F, G being XFinSequence of D
for b being BinOp of D
for bFG being XFinSequence of D st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ) holds
b "**" (F ^ G) = b "**" bFG
let F, G be XFinSequence of D; :: thesis: for b being BinOp of D
for bFG being XFinSequence of D st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ) holds
b "**" (F ^ G) = b "**" bFG
let b be BinOp of D; :: thesis: for bFG being XFinSequence of D st b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ) holds
b "**" (F ^ G) = b "**" bFG
let bFG be XFinSequence of D; :: thesis: ( b is commutative & b is associative & ( b is having_a_unity or len F >= 1 ) & len F = len G & len F = len bFG & ( for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ) implies b "**" (F ^ G) = b "**" bFG )
assume that
A1: ( b is commutative & b is associative ) and
A2: ( b is having_a_unity or len F >= 1 ) and
A3: len F = len G and
A4: len F = len bFG and
A5: for n being Nat st n in dom bFG holds
bFG . n = b . ((F . n),(G . n)) ; :: thesis: b "**" (F ^ G) = b "**" bFG
set xG = XFS2FS G;
set xF = XFS2FS F;
A6: ( b "**" F = b "**" (XFS2FS F) & b "**" G = b "**" (XFS2FS G) ) by A2, A3, Th43;
set xb = XFS2FS bFG;
A7: len (XFS2FS bFG) = len bFG by AFINSQ_1:def 9;
A8: for k being Nat st k in dom (XFS2FS bFG) holds
(XFS2FS bFG) . k = b . (((XFS2FS F) . k),((XFS2FS G) . k))

proof

let k be Nat; :: thesis: ( k in dom (XFS2FS bFG) implies (XFS2FS bFG) . k = b . (((XFS2FS F) . k),((XFS2FS G) . k)) )
assume A9: k in dom (XFS2FS bFG) ; :: thesis: (XFS2FS bFG) . k = b . (((XFS2FS F) . k),((XFS2FS G) . k))
k in Seg (len (XFS2FS bFG)) by A9, FINSEQ_1:def 3;
then k >= 1 by FINSEQ_1:1;
then reconsider k1 = k - 1 as Element of NAT by NAT_1:21;
A10: k in Seg (len (XFS2FS bFG)) by A9, FINSEQ_1:def 3;
then A11: 1 <= k by FINSEQ_1:1;
k in Seg (len (XFS2FS bFG)) by A9, FINSEQ_1:def 3;
then ( k1 < k1 + 1 & k <= len (XFS2FS bFG) ) by FINSEQ_1:1, NAT_1:13;
then k1 < len (XFS2FS bFG) by XXREAL_0:2;
then k1 in dom bFG by A7, AFINSQ_1:86;
then A13: bFG . k1 = b . ((F . k1),(G . k1)) by A5;
A14: k <= len bFG by A7, A10, FINSEQ_1:1;
then ( bFG . (k - 1) = (XFS2FS bFG) . k & F . (k - 1) = (XFS2FS F) . k ) by A4, A11, AFINSQ_1:def 9;
hence (XFS2FS bFG) . k = b . (((XFS2FS F) . k),((XFS2FS G) . k)) by A3, A4, A11, A14, A13, AFINSQ_1:def 9; :: thesis: verum

end;

( len (XFS2FS F) = len F & len G = len (XFS2FS G) ) by AFINSQ_1:def 9;
then b "**" (XFS2FS bFG) = b . ((b "**" (XFS2FS F)),(b "**" (XFS2FS G))) by A1, A2, A3, A4, A7, A8, FINSOP_1:9;
then b "**" bFG = b . ((b "**" F),(b "**" G)) by A2, A4, A6, Th43;
hence b "**" (F ^ G) = b "**" bFG by A1, A2, A3, Th41; :: thesis: verum