let S be standard-ins AMI-Struct of IL,N; :: thesis: ( S is regular implies S is homogeneous )
assume A1: for T being InsType of S holds AddressParts T is product-like ; :: according to AMISTD_2:def 11 :: thesis: S is homogeneous
let I, J be Instruction of S; :: according to AMISTD_2:def 4 :: thesis: ( InsCode I = InsCode J implies dom (AddressPart I) = dom (AddressPart J) )
assume A2: InsCode I = InsCode J ; :: thesis: dom (AddressPart I) = dom (AddressPart J)
AddressParts (InsCode I) is product-like by A1;
then consider f being Function such that
A3: AddressParts (InsCode I) = product f by CARD_3:def 14;
A4: ( AddressPart I in AddressParts (InsCode I) & AddressPart J in AddressParts (InsCode I) ) by A2;
hence dom (AddressPart I) = dom f by A3, CARD_3:18
.= dom (AddressPart J) by A3, A4, CARD_3:18 ;
:: thesis: verum