let D be non empty set ; :: thesis: for F, G being FinSequence of D
for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
g "**" (F ^ G) = g . (g "**" F),(g "**" G)
let F, G be FinSequence of D; :: thesis: for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) holds
g "**" (F ^ G) = g . (g "**" F),(g "**" G)
let g be BinOp of D; :: thesis: ( g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies g "**" (F ^ G) = g . (g "**" F),(g "**" G) )
defpred S₁[ FinSequence of D] means for F being FinSequence of D
for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len $1 >= 1 ) ) holds
g "**" (F ^ $1) = g . (g "**" F),(g "**" $1);
A1: for G being FinSequence of D
for d being Element of D st S₁[G] holds
S₁[G ^ <*d*>]

proof

let G be FinSequence of D; :: thesis: for d being Element of D st S₁[G] holds
S₁[G ^ <*d*>]
let d be Element of D; :: thesis: ( S₁[G] implies S₁[G ^ <*d*>] )
assume A2: S₁[G] ; :: thesis: S₁[G ^ <*d*>]
let F be FinSequence of D; :: thesis: for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len (G ^ <*d*>) >= 1 ) ) holds
g "**" (F ^ (G ^ <*d*>)) = g . (g "**" F),(g "**" (G ^ <*d*>))
let g be BinOp of D; :: thesis: ( g is associative & ( g is having_a_unity or ( len F >= 1 & len (G ^ <*d*>) >= 1 ) ) implies g "**" (F ^ (G ^ <*d*>)) = g . (g "**" F),(g "**" (G ^ <*d*>)) )
assume that
A3: g is associative and
A4: ( g is having_a_unity or ( len F >= 1 & len (G ^ <*d*>) >= 1 ) ) ; :: thesis: g "**" (F ^ (G ^ <*d*>)) = g . (g "**" F),(g "**" (G ^ <*d*>))

A5: now

A6: len (F ^ G) = (len F) + (len G) by FINSEQ_1:35;
assume not g is having_a_unity ; :: thesis: len (F ^ G) >= 1
hence len (F ^ G) >= 1 by A4, A6, NAT_1:12; :: thesis: verum

end;

A7: g "**" (F ^ (G ^ <*d*>)) = g "**" ((F ^ G) ^ <*d*>) by FINSEQ_1:45
.= g . (g "**" (F ^ G)),d by A5, Th5 ;

now

per cases ( len G <> 0 or len G = 0 ) ;

suppose A8: len G <> 0 ; :: thesis: g "**" (F ^ (G ^ <*d*>)) = g . (g "**" F),(g "**" (G ^ <*d*>))

then len G >= 1 by NAT_1:14;
hence g "**" (F ^ (G ^ <*d*>)) = g . (g . (g "**" F),(g "**" G)),d by A2, A3, A4, A7
.= g . (g "**" F),(g . (g "**" G),d) by A3, BINOP_1:def 3
.= g . (g "**" F),(g "**" (G ^ <*d*>)) by A8, Th5, NAT_1:14 ;
:: thesis: verum

end;

suppose len G = 0 ; :: thesis: g "**" (F ^ (G ^ <*d*>)) = g . (g "**" F),(g "**" (G ^ <*d*>))

then A9: G = {} ;
hence g "**" (F ^ (G ^ <*d*>)) = g "**" (F ^ <*d*>) by FINSEQ_1:47
.= g . (g "**" F),d by A4, Th5
.= g . (g "**" F),(g "**" <*d*>) by Lm4
.= g . (g "**" F),(g "**" (G ^ <*d*>)) by A9, FINSEQ_1:47 ;
:: thesis: verum

end;

end;

end;

hence g "**" (F ^ (G ^ <*d*>)) = g . (g "**" F),(g "**" (G ^ <*d*>)) ; :: thesis: verum

end;

A10: S₁[ <*> D]

proof

let F be FinSequence of D; :: thesis: for g being BinOp of D st g is associative & ( g is having_a_unity or ( len F >= 1 & len (<*> D) >= 1 ) ) holds
g "**" (F ^ (<*> D)) = g . (g "**" F),(g "**" (<*> D))
let g be BinOp of D; :: thesis: ( g is associative & ( g is having_a_unity or ( len F >= 1 & len (<*> D) >= 1 ) ) implies g "**" (F ^ (<*> D)) = g . (g "**" F),(g "**" (<*> D)) )
assume that
g is associative and
A11: ( g is having_a_unity or ( len F >= 1 & len (<*> D) >= 1 ) ) ; :: thesis: g "**" (F ^ (<*> D)) = g . (g "**" F),(g "**" (<*> D))
thus g "**" (F ^ (<*> D)) = g "**" F by FINSEQ_1:47
.= g . (g "**" F),(the_unity_wrt g) by A11, SETWISEO:23
.= g . (g "**" F),(g "**" (<*> D)) by A11, Lm3 ; :: thesis: verum

end;

for G being FinSequence of D holds S₁[G] from FINSEQ_2:sch 2(A10, A1);
hence ( g is associative & ( g is having_a_unity or ( len F >= 1 & len G >= 1 ) ) implies g "**" (F ^ G) = g . (g "**" F),(g "**" G) ) ; :: thesis: verum