now

let x be set ; :: thesis: ( x in dom (s +* (l,i)) implies (s +* (l,i)) . b₁ in the Object-Kind of S . b₁ )
assume A1: x in dom (s +* (l,i)) ; :: thesis: (s +* (l,i)) . b₁ in the Object-Kind of S . b₁
A2: x in dom s by A1, FUNCT_7:32;

per cases ( x = l or x <> l ) ;

suppose A3: x = l ; :: thesis: (s +* (l,i)) . b₁ in the Object-Kind of S . b₁

then A4: the Object-Kind of S . x = the Instructions of S by Def8;
A5: l in NAT ;
NAT c= the carrier of S by Def2;
then l in the carrier of S by A5;
then l in dom s by PARTFUN1:def 4;
then (s +* (l,i)) . x = i by A3, FUNCT_7:33;
hence (s +* (l,i)) . x in the Object-Kind of S . x by A4; :: thesis: verum

end;

suppose x <> l ; :: thesis: (s +* (l,i)) . b₁ in the Object-Kind of S . b₁

then (s +* (l,i)) . x = s . x by FUNCT_7:34;
hence (s +* (l,i)) . x in the Object-Kind of S . x by A2, FUNCT_1:def 20; :: thesis: verum

end;

end;

end;

hence s +* (l,i) is State of S by FUNCT_1:def 20; :: thesis: verum