A1: dom (s +* l,i) = dom s by FUNCT_7:32;
A2: dom s = dom the Object-Kind of S by CARD_3:18;

now

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

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

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

then A5: (s +* l,i) . x = i by A2, A3, FUNCT_7:33;
the Object-Kind of S . x = ObjectKind l by A4
.= the Instructions of S by Def14 ;
hence (s +* l,i) . x in the Object-Kind of S . x by A5; :: 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 A3, CARD_3:18; :: thesis: verum

end;

end;

end;

hence s +* l,i is State of S by A1, A2, CARD_3:18; :: thesis: verum