let D be non empty set ; :: thesis: for b being BinOp of D
for F, G, bFG being XFinSequence of 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 Element of 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 F, G, bFG being XFinSequence of 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 Element of NAT st n in dom bFG holds
bFG . n = b . (F . n),(G . n) ) holds
b "**" (F ^ G) = b "**" bFG
let F, G, bFG be XFinSequence of ; :: 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 Element of 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 & len F = len bFG ) and
A4: for n being Element of NAT st n in dom bFG holds
bFG . n = b . (F . n),(G . n) ; :: thesis: b "**" (F ^ G) = b "**" bFG
set xF = XFS2FS F;
set xG = XFS2FS G;
set xb = XFS2FS bFG;
A5: ( len (XFS2FS F) = len F & len G = len (XFS2FS G) & len (XFS2FS bFG) = len bFG ) by PRGCOR_2:def 2;
for k being Element of NAT st k in dom (XFS2FS bFG) holds
(XFS2FS bFG) . k = b . ((XFS2FS F) . k),((XFS2FS G) . k)

proof

let k be Element of NAT ; :: thesis: ( k in dom (XFS2FS bFG) implies (XFS2FS bFG) . k = b . ((XFS2FS F) . k),((XFS2FS G) . k) )
assume A6: k in dom (XFS2FS bFG) ; :: thesis: (XFS2FS bFG) . k = b . ((XFS2FS F) . k),((XFS2FS G) . k)
k in Seg (len (XFS2FS bFG)) by A6, FINSEQ_1:def 3;
then k >= 1 by FINSEQ_1:3;
then reconsider k1 = k - 1 as Element of NAT by NAT_1:21;
k in Seg (len (XFS2FS bFG)) by A6, FINSEQ_1:def 3;
then ( k1 < k1 + 1 & k <= len (XFS2FS bFG) ) by FINSEQ_1:3, NAT_1:13;
then k1 < len (XFS2FS bFG) by XXREAL_0:2;
then ( k1 in len bFG & k in Seg (len (XFS2FS bFG)) ) by A5, A6, FINSEQ_1:def 3, NAT_1:45;
then ( k1 in dom bFG & 1 <= k & k <= len bFG ) by A5, FINSEQ_1:3;
then ( bFG . k1 = b . (F . k1),(G . k1) & bFG . (k -' 1) = (XFS2FS bFG) . k & F . (k -' 1) = (XFS2FS F) . k & G . (k -' 1) = (XFS2FS G) . k & k1 = k -' 1 ) by A3, A4, PRGCOR_2:def 2, XREAL_1:235;
hence (XFS2FS bFG) . k = b . ((XFS2FS F) . k),((XFS2FS G) . k) ; :: thesis: verum

end;

then ( b "**" (XFS2FS bFG) = b . (b "**" (XFS2FS F)),(b "**" (XFS2FS G)) & b "**" F = b "**" (XFS2FS F) & b "**" G = b "**" (XFS2FS G) ) by A1, A2, A3, A5, Th47, FINSOP_1:10;
then b "**" bFG = b . (b "**" F),(b "**" G) by A2, A3, Th47;
hence b "**" (F ^ G) = b "**" bFG by A1, A2, A3, STIRL2_1:47; :: thesis: verum