let n be Nat; :: thesis: for X being set
for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A (/\) A1)) . n = A /\ ((superior_setsequence A1) . n)
let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X holds (superior_setsequence (A (/\) A1)) . n = A /\ ((superior_setsequence A1) . n)
let A be Subset of X; :: thesis: for A1 being SetSequence of X holds (superior_setsequence (A (/\) A1)) . n = A /\ ((superior_setsequence A1) . n)
let A1 be SetSequence of X; :: thesis: (superior_setsequence (A (/\) A1)) . n = A /\ ((superior_setsequence A1) . n)
(superior_setsequence (A (/\) A1)) . n = Union ((A (/\) A1) ^\ n) by Th2
.= Union (A (/\) (A1 ^\ n)) by Th16
.= A /\ (Union (A1 ^\ n)) by Th38
.= A /\ ((superior_setsequence A1) . n) by Th2 ;
hence (superior_setsequence (A (/\) A1)) . n = A /\ ((superior_setsequence A1) . n) ; :: thesis: verum