let n be Nat; :: thesis: for X being set
for A1, A2 being SetSequence of X holds (superior_setsequence (A1 (\/) A2)) . n = ((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 = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n)
let A1, A2 be SetSequence of X; :: thesis: (superior_setsequence (A1 (\/) A2)) . n = ((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 Th5
.= (Union (A1 ^\ n)) \/ (Union (A2 ^\ n)) by Th9
.= ((superior_setsequence A1) . n) \/ (Union (A2 ^\ n)) by Th2 ;
hence (superior_setsequence (A1 (\/) A2)) . n = ((superior_setsequence A1) . n) \/ ((superior_setsequence A2) . n) by Th2; :: thesis: verum