per cases ( i in Seg n or not i in Seg n ) ;

suppose A1: i in Seg n ; :: thesis: ( ( i in Seg n implies scale . i is Element of HPS ) & ( not i in Seg n implies the Element of HPS is Element of HPS ) & ( for b₁ being Element of HPS holds verum ) )

scale is Element of Funcs ((Seg n), the carrier of HPS) by FINSEQ_2:93;
then ( dom scale = Seg n & rng scale c= the carrier of HPS ) by FUNCT_2:92;
then scale . i in rng scale by A1, FUNCT_1:def 3;
hence ( ( i in Seg n implies scale . i is Element of HPS ) & ( not i in Seg n implies the Element of HPS is Element of HPS ) & ( for b₁ being Element of HPS holds verum ) ) ; :: thesis: verum

end;

suppose not i in Seg n ; :: thesis: ( ( i in Seg n implies scale . i is Element of HPS ) & ( not i in Seg n implies the Element of HPS is Element of HPS ) & ( for b₁ being Element of HPS holds verum ) )

hence ( ( i in Seg n implies scale . i is Element of HPS ) & ( not i in Seg n implies the Element of HPS is Element of HPS ) & ( for b₁ being Element of HPS holds verum ) ) ; :: thesis: verum

end;

end;