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 :: thesis: ( not g is having_a_unity implies len (F ^ G) >= 1 )

A6: len (F ^ G) = (len F) + (len G) by FINSEQ_1:22;
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:32
.= g . ((g "**" (F ^ G)),d) by A5, Th4 ;

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

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, Th4, 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:34
.= g . ((g "**" F),d) by A4, Th4
.= g . ((g "**" F),(g "**" <*d*>)) by Lm4
.= g . ((g "**" F),(g "**" (G ^ <*d*>))) by A9, FINSEQ_1:34 ;
:: 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:34
.= g . ((g "**" F),(the_unity_wrt g)) by A11, SETWISEO:15
.= 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