let n be Element of NAT ; :: thesis: for X being set
for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\+\) A2)) . n
let X be set ; :: thesis: for A1, A2 being SetSequence of X holds ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\+\) A2)) . n
let A1, A2 be SetSequence of X; :: thesis: ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\+\) A2)) . n
((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) = (Union (A1 ^\ n)) \+\ ((superior_setsequence A2) . n) by Th2
.= (Union (A1 ^\ n)) \+\ (Union (A2 ^\ n)) by Th2 ;
then ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= Union ((A1 ^\ n) (\+\) (A2 ^\ n)) by Th11;
then ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= Union ((A1 (\+\) A2) ^\ n) by Th7;
hence ((superior_setsequence A1) . n) \+\ ((superior_setsequence A2) . n) c= (superior_setsequence (A1 (\+\) A2)) . n by Th2; :: thesis: verum