dom s = the carrier of A by AMI_1:79;
then s +* o,a = s +* (o .--> a) by FUNCT_7:def 3;
hence s +* o,a is State of A ; :: thesis: verum