set n = 4;
consider I being SortSymbol of S such that
A1: ( I = 1 & the connectives of S . 4 is_of_type {} ,I & the Sorts of A . I = INT ) and
( (Den ((In (( the connectives of S . 4), the carrier' of S)),A)) . {} = 0 & (Den ((In (( the connectives of S . (4 + 1)), the carrier' of S)),A)) . {} = 1 & ( for i, j being Integer holds
( (Den ((In (( the connectives of S . (4 + 2)), the carrier' of S)),A)) . <*i*> = - i & (Den ((In (( the connectives of S . (4 + 3)), the carrier' of S)),A)) . <*i,j*> = i + j & (Den ((In (( the connectives of S . (4 + 4)), the carrier' of S)),A)) . <*i,j*> = i * j & ( j <> 0 implies (Den ((In (( the connectives of S . (4 + 5)), the carrier' of S)),A)) . <*i,j*> = i div j ) & (Den ((In (( the connectives of S . (4 + 6)), the carrier' of S)),A)) . <*i,j*> = IFGT (i,j,FALSE,TRUE) ) ) ) by Def49;
thus for b₁ being Element of the Sorts of A . 1 holds b₁ is integer by A1; :: thesis: verum