let D be non empty set ; 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; 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; ( 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 S1[ 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 S1[G] holds
S1[G ^ <*d*>]
proof
let G be
FinSequence of
D;
for d being Element of D st S1[G] holds
S1[G ^ <*d*>]let d be
Element of
D;
( S1[G] implies S1[G ^ <*d*>] )
assume A2:
S1[
G]
;
S1[G ^ <*d*>]
let F be
FinSequence of
D;
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;
( 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 ) )
;
g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>)))
A7:
g "**" (F ^ (G ^ <*d*>)) =
g "**" ((F ^ G) ^ <*d*>)
by FINSEQ_1:32
.=
g . (
(g "**" (F ^ G)),
d)
by A5, Th4
;
now g "**" (F ^ (G ^ <*d*>)) = g . ((g "**" F),(g "**" (G ^ <*d*>)))per cases
( len G <> 0 or len G = 0 )
;
suppose A8:
len G <> 0
;
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
;
verum end; end; end;
hence
g "**" (F ^ (G ^ <*d*>)) = g . (
(g "**" F),
(g "**" (G ^ <*d*>)))
;
verum
end;
A10:
S1[ <*> D]
for G being FinSequence of D holds S1[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)) )
; verum