let n be Nat; :: thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds A \+\ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\+\) A1)) . n
let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds A \+\ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\+\) A1)) . n
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds A \+\ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\+\) A1)) . n
let A1 be SetSequence of X; :: thesis: A \+\ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\+\) A1)) . n
A \+\ ((superior_setsequence A1) . n) = A \+\ (Union (A1 ^\ n)) by Th2;
then A \+\ ((superior_setsequence A1) . n) c= Union (A (\+\) (A1 ^\ n)) by Th42;
then A \+\ ((superior_setsequence A1) . n) c= Union ((A (\+\) A1) ^\ n) by Th20;
hence A \+\ ((superior_setsequence A1) . n) c= (superior_setsequence (A (\+\) A1)) . n by Th2; :: thesis: verum