let O, E be set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (Product (F,A)) .: Y c= Y

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; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: (Product (F,A)) .: Y c= Y

per cases
( O = {} or O <> {} )
;

end;

suppose
O = {}
; :: thesis: (Product (F,A)) .: Y c= Y

then
len F = 0
;

then Product (F,A) = id E by Def3;

hence (Product (F,A)) .: Y c= Y by FUNCT_1:92; :: thesis: verum

end;then Product (F,A) = id E by Def3;

hence (Product (F,A)) .: Y c= Y by FUNCT_1:92; :: thesis: verum

suppose A2:
O <> {}
; :: thesis: (Product (F,A)) .: Y c= Y

defpred S_{1}[ 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 S_{1}[k] holds

S_{1}[k + 1]

A9: k = len F ;

A10: S_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A10, A3);

hence (Product (F,A)) .: Y c= Y by A9; :: thesis: verum

end;(Product (F,A)) .: Y c= Y;

A3: for k being Nat st S

S

proof

reconsider k = len F as Element of NAT ;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A4: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A4: S

now :: thesis: for F being FinSequence of O st len F = k + 1 holds

(Product (F,A)) .: Y c= Y

hence
S(Product (F,A)) .: Y c= Y

let F be FinSequence of O; :: thesis: ( len F = k + 1 implies (Product (F,A)) .: Y c= Y )

assume A5: len F = k + 1 ; :: thesis: (Product (F,A)) .: Y c= Y

then 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; :: thesis: verum

end;assume A5: len F = k + 1 ; :: thesis: (Product (F,A)) .: Y c= Y

then 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; :: thesis: verum

A9: k = len F ;

A10: S

proof

for k being Nat holds S
let F be FinSequence of O; :: thesis: ( len F = 0 implies (Product (F,A)) .: Y c= Y )

assume len F = 0 ; :: thesis: (Product (F,A)) .: Y c= Y

then Product (F,A) = id E by Def3;

hence (Product (F,A)) .: Y c= Y by FUNCT_1:92; :: thesis: verum

end;assume len F = 0 ; :: thesis: (Product (F,A)) .: Y c= Y

then Product (F,A) = id E by Def3;

hence (Product (F,A)) .: Y c= Y by FUNCT_1:92; :: thesis: verum

hence (Product (F,A)) .: Y c= Y by A9; :: thesis: verum