let n be Nat; :: thesis: for X being set
for A1, A2 being SetSequence of X holds (superior_setsequence (A1 (/\) A2)) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)
let X be set ; :: thesis: for A1, A2 being SetSequence of X holds (superior_setsequence (A1 (/\) A2)) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)
let A1, A2 be SetSequence of X; :: thesis: (superior_setsequence (A1 (/\) A2)) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n)
(superior_setsequence (A1 (/\) A2)) . n = Union ((A1 (/\) A2) ^\ n) by Th2
.= Union ((A1 ^\ n) (/\) (A2 ^\ n)) by Th4 ;
then (superior_setsequence (A1 (/\) A2)) . n c= (Union (A1 ^\ n)) /\ (Union (A2 ^\ n)) by Th8;
then (superior_setsequence (A1 (/\) A2)) . n c= ((superior_setsequence A1) . n) /\ (Union (A2 ^\ n)) by Th2;
hence (superior_setsequence (A1 (/\) A2)) . n c= ((superior_setsequence A1) . n) /\ ((superior_setsequence A2) . n) by Th2; :: thesis: verum