let n be Nat; :: thesis: for X being set
for B being SetSequence of X st B is V56() holds
(inferior_setsequence B) . n = B . n
let X be set ; :: thesis: for B being SetSequence of X st B is V56() holds
(inferior_setsequence B) . n = B . n
let B be SetSequence of X; :: thesis: ( B is V56() implies (inferior_setsequence B) . n = B . n )
assume B is V56() ; :: thesis: (inferior_setsequence B) . n = B . n
then ((inferior_setsequence B) . (n + 1)) /\ (B . n) = B . n by Th44, XBOOLE_1:28;
hence (inferior_setsequence B) . n = B . n by Th21; :: thesis: verum