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

end;

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

defpred S₁[ Element of NAT ] means for F being FinSequence of O st len F = $1 holds
(Product F,A) .: Y c= Y;
A3: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

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

now

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:22;
len F = (len Fk) + (len <*o*>) by A6, FINSEQ_1:35;
then k + 1 = (len Fk) + 1 by A5, FINSEQ_1:56;
then A7: (Product Fk,A) .: Y c= Y by A4;
reconsider F1 = <*o*> as FinSequence of O by A6, FINSEQ_1:50;
Product F,A = (Product Fk,A) * (Product F1,A) by A2, A6, Lm29;
then A8: (Product F,A) .: Y = (Product Fk,A) .: ((Product F1,A) .: Y) by RELAT_1:159;
Product F1,A = A . o by A2, Lm26;
then (Product F1,A) .: Y c= Y by A1, A2, Def1;
then (Product F,A) .: Y c= (Product Fk,A) .: Y by A8, RELAT_1:156;
hence (Product F,A) .: Y c= Y by A7, XBOOLE_1:1; :: 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:162; :: thesis: verum

end;

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

end;

end;