let n be Nat; :: thesis: for X being set
for A1, A2 being SetSequence of X holds (inferior_setsequence (A1 (\) A2)) . n c= ((inferior_setsequence A1) . n) \ ((inferior_setsequence A2) . n)
let X be set ; :: thesis: for A1, A2 being SetSequence of X holds (inferior_setsequence (A1 (\) A2)) . n c= ((inferior_setsequence A1) . n) \ ((inferior_setsequence A2) . n)
let A1, A2 be SetSequence of X; :: thesis: (inferior_setsequence (A1 (\) A2)) . n c= ((inferior_setsequence A1) . n) \ ((inferior_setsequence A2) . n)
(inferior_setsequence (A1 (\) A2)) . n = Intersection ((A1 (\) A2) ^\ n) by Th1
.= Intersection ((A1 ^\ n) (\) (A2 ^\ n)) by Th6 ;
then (inferior_setsequence (A1 (\) A2)) . n c= (Intersection (A1 ^\ n)) \ (Intersection (A2 ^\ n)) by Th14;
then (inferior_setsequence (A1 (\) A2)) . n c= ((inferior_setsequence A1) . n) \ (Intersection (A2 ^\ n)) by Th1;
hence (inferior_setsequence (A1 (\) A2)) . n c= ((inferior_setsequence A1) . n) \ ((inferior_setsequence A2) . n) by Th1; :: thesis: verum