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