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 b1 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 b1 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 b1 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 b1 being Element of HPS holds verum ) ) ; :: thesis: verum
end;
end;