let X be set ; :: thesis: for B being SetSequence of X st B is V56() holds

inferior_setsequence B = B

let B be SetSequence of X; :: thesis: ( B is V56() implies inferior_setsequence B = B )

assume B is V56() ; :: thesis: inferior_setsequence B = B

then for n being Nat holds (inferior_setsequence B) . n = B . n by Th45;

then for n being Element of NAT holds (inferior_setsequence B) . n = B . n ;

hence inferior_setsequence B = B by FUNCT_2:63; :: thesis: verum

inferior_setsequence B = B

let B be SetSequence of X; :: thesis: ( B is V56() implies inferior_setsequence B = B )

assume B is V56() ; :: thesis: inferior_setsequence B = B

then for n being Nat holds (inferior_setsequence B) . n = B . n by Th45;

then for n being Element of NAT holds (inferior_setsequence B) . n = B . n ;

hence inferior_setsequence B = B by FUNCT_2:63; :: thesis: verum