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 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; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[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) + () by ;
then k + 1 = (len Fk) + 1 by ;
then A7: (Product (Fk,A)) .: Y c= Y by A4;
reconsider F1 = <*o*> as FinSequence of O by ;
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 ;
then (Product (F1,A)) .: Y c= Y by A1, A2;
then (Product (F,A)) .: Y c= (Product (Fk,A)) .: Y by ;
hence (Product (F,A)) .: Y c= Y by A7; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
reconsider k = len F as Element of NAT ;
A9: k = len F ;
A10: S1[ 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 S1[k] from NAT_1:sch 2(A10, A3);
hence (Product (F,A)) .: Y c= Y by A9; :: thesis: verum
end;
end;