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