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

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

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;

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

defpred S₁[ 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₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: for F being FinSequence of O st len F = k + 1 holds
(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;

hence S₁[k + 1] ; :: thesis: verum

end;

reconsider k = len F as Element of NAT ;
A9: k = len F ;
A10: S₁[ 0 ]

proof

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;

for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A3);
hence (Product (F,A)) .: Y c= Y by A9; :: thesis: verum

end;

end;