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