i1,i2 --> I1,I2 = (i1 .--> I1) +* (i2 .--> I2) by FUNCT_4:def 4;
hence i1,i2 --> I1,I2 is FinPartState of S ; :: thesis: verum