A1: ObjectKind i1 = the Instructions of S by AMI_1:def 14;
ObjectKind i2 = the Instructions of S by AMI_1:def 14;
hence i1,i2 --> I1,I2 is FinPartState of by A1, AMI_1:58; :: thesis: verum