let D be non empty set ; :: thesis: for A being BinOp of D
for F, G being D * -valued FinSequence holds A "**" (F ^ G) = (A "**" F) ^ (A "**" G)
let A be BinOp of D; :: thesis: for F, G being D * -valued FinSequence holds A "**" (F ^ G) = (A "**" F) ^ (A "**" G)
let F, G be D * -valued FinSequence; :: thesis: A "**" (F ^ G) = (A "**" F) ^ (A "**" G)
set FG = F ^ G;
A1: ( len (A "**" F) = len F & len (A "**" G) = len G ) by CARD_1:def 7;
A2: ( len (A "**" (F ^ G)) = len (F ^ G) & len (F ^ G) = (len F) + (len G) ) by CARD_1:def 7, FINSEQ_1:22;
for n being Nat st 1 <= n & n <= (len F) + (len G) holds
(A "**" (F ^ G)) . n = ((A "**" F) ^ (A "**" G)) . n

proof

let n be Nat; :: thesis: ( 1 <= n & n <= (len F) + (len G) implies (A "**" (F ^ G)) . n = ((A "**" F) ^ (A "**" G)) . n )
assume A3: ( 1 <= n & n <= (len F) + (len G) ) ; :: thesis: (A "**" (F ^ G)) . n = ((A "**" F) ^ (A "**" G)) . n

per cases ( n in dom F or ex k being Nat st
( k in dom G & n = (len F) + k ) ) by FINSEQ_1:25, A3, A2, FINSEQ_3:25;

suppose A4: n in dom F ; :: thesis: (A "**" (F ^ G)) . n = ((A "**" F) ^ (A "**" G)) . n

then n in dom (A "**" F) by A1, FINSEQ_3:29;
hence ((A "**" F) ^ (A "**" G)) . n = (A "**" F) . n by FINSEQ_1:def 7
.= A "**" (F . n) by A4, Def10
.= A "**" ((F ^ G) . n) by A4, FINSEQ_1:def 7
.= (A "**" (F ^ G)) . n by A3, A2, FINSEQ_3:25, Def10 ;
:: thesis: verum

end;

suppose ex k being Nat st
( k in dom G & n = (len F) + k ) ; :: thesis: (A "**" (F ^ G)) . n = ((A "**" F) ^ (A "**" G)) . n

then consider k being Nat such that
A5: ( k in dom G & n = (len F) + k ) ;
k in dom (A "**" G) by A5, A1, FINSEQ_3:29;
hence ((A "**" F) ^ (A "**" G)) . n = (A "**" G) . k by A1, A5, FINSEQ_1:def 7
.= A "**" (G . k) by A5, Def10
.= A "**" ((F ^ G) . n) by A5, FINSEQ_1:def 7
.= (A "**" (F ^ G)) . n by A3, A2, FINSEQ_3:25, Def10 ;
:: thesis: verum

end;

end;

end;

hence A "**" (F ^ G) = (A "**" F) ^ (A "**" G) by CARD_1:def 7, A2; :: thesis: verum