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: 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 A2: ( g is associative & ( 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 A2, SETWISEO:23
.= g . (g "**" F),(g "**" (<*> D)) by A2, Lm3 ; :: thesis: verum

end;

A3: 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 A4: 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 A5: ( g is associative & ( g is having_a_unity or ( len F >= 1 & len (G ^ <*d*>) >= 1 ) ) ) ; :: thesis: g "**" (F ^ (G ^ <*d*>)) = g . (g "**" F),(g "**" (G ^ <*d*>))

A6: now

assume not g is having_a_unity ; :: thesis: len (F ^ G) >= 1
then ( len F >= 1 & len (F ^ G) = (len F) + (len G) & (len F) + (len G) >= len F ) by A5, FINSEQ_1:35, NAT_1:12;
hence len (F ^ G) >= 1 by XXREAL_0:2; :: thesis: verum

end;

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

now

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

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

then A8: len G >= 1 by NAT_1:14;
hence g "**" (F ^ (G ^ <*d*>)) = g . (g . (g "**" F),(g "**" G)),d by A4, A5, A7
.= g . (g "**" F),(g . (g "**" G),d) by A5, BINOP_1:def 3
.= g . (g "**" F),(g "**" (G ^ <*d*>)) by A8, Th5 ;
:: 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 A5, 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;

for G being FinSequence of D holds S₁[G] from FINSEQ_2:sch 2(A1, A3);
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