let O, E be set ; for F being FinSequence of O
for Y being Subset of E
for A being Action of O,E st Y is_stable_under_the_action_of A holds
(Product (F,A)) .: Y c= Y
let F be FinSequence of O; for Y being Subset of E
for A being Action of O,E st Y is_stable_under_the_action_of A holds
(Product (F,A)) .: Y c= Y
let Y be Subset of E; for A being Action of O,E st Y is_stable_under_the_action_of A holds
(Product (F,A)) .: Y c= Y
let A be Action of O,E; ( Y is_stable_under_the_action_of A implies (Product (F,A)) .: Y c= Y )
assume A1:
Y is_stable_under_the_action_of A
; (Product (F,A)) .: Y c= Y
per cases
( O = {} or O <> {} )
;
suppose A2:
O <> {}
;
(Product (F,A)) .: Y c= Ydefpred S1[
Nat]
means for
F being
FinSequence of
O st
len F = $1 holds
(Product (F,A)) .: Y c= Y;
A3:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
S1[k + 1]
now for F being FinSequence of O st len F = k + 1 holds
(Product (F,A)) .: Y c= Ylet F be
FinSequence of
O;
( len F = k + 1 implies (Product (F,A)) .: Y c= Y )assume A5:
len F = k + 1
;
(Product (F,A)) .: Y c= Ythen consider Fk being
FinSequence of
O,
o being
Element of
O such that A6:
F = Fk ^ <*o*>
by FINSEQ_2:19;
len F = (len Fk) + (len <*o*>)
by A6, FINSEQ_1:22;
then
k + 1
= (len Fk) + 1
by A5, FINSEQ_1:39;
then A7:
(Product (Fk,A)) .: Y c= Y
by A4;
reconsider F1 =
<*o*> as
FinSequence of
O by A6, FINSEQ_1:36;
Product (
F,
A)
= (Product (Fk,A)) * (Product (F1,A))
by A2, A6, Lm28;
then A8:
(Product (F,A)) .: Y = (Product (Fk,A)) .: ((Product (F1,A)) .: Y)
by RELAT_1:126;
Product (
F1,
A)
= A . o
by A2, Lm25;
then
(Product (F1,A)) .: Y c= Y
by A1, A2;
then
(Product (F,A)) .: Y c= (Product (Fk,A)) .: Y
by A8, RELAT_1:123;
hence
(Product (F,A)) .: Y c= Y
by A7;
verum end;
hence
S1[
k + 1]
;
verum
end; reconsider k =
len F as
Element of
NAT ;
A9:
k = len F
;
A10:
S1[
0 ]
for
k being
Nat holds
S1[
k]
from NAT_1:sch 2(A10, A3);
hence
(Product (F,A)) .: Y c= Y
by A9;
verum end;