let N be non empty with_non-empty_elements set ; :: thesis: for A being non empty IC-Ins-separated AMI-Struct of N
for I being Instruction of A
for o being Object of A st ObjectKind o is trivial holds
not o in Out_U_Inp I
let A be non empty IC-Ins-separated AMI-Struct of N; :: thesis: for I being Instruction of A
for o being Object of A st ObjectKind o is trivial holds
not o in Out_U_Inp I
let I be Instruction of A; :: thesis: for o being Object of A st ObjectKind o is trivial holds
not o in Out_U_Inp I
let o be Object of A; :: thesis: ( ObjectKind o is trivial implies not o in Out_U_Inp I )
assume A1: ObjectKind o is trivial ; :: thesis: not o in Out_U_Inp I
assume o in Out_U_Inp I ; :: thesis: contradiction
then consider s being State of A, a being Element of ObjectKind o such that
A2: Exec (I,(s +* (o,a))) <> (Exec (I,s)) +* (o,a) by Def5;
s . o is Element of ObjectKind o by MEMSTR_0:77;
then s . o = a by A1, ZFMISC_1:def 10;
then A3: Exec (I,(s +* (o,a))) = Exec (I,s) by FUNCT_7:35;
A4: dom (Exec (I,s)) = the carrier of A by PARTFUN1:def 2;
A5: for x being set st x in the carrier of A holds
((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x

proof

let x be set ; :: thesis: ( x in the carrier of A implies ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x )
assume x in the carrier of A ; :: thesis: ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x

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

suppose A6: x = o ; :: thesis: ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x

A7: (Exec (I,s)) . o is Element of ObjectKind o by MEMSTR_0:77;
thus ((Exec (I,s)) +* (o,a)) . x = a by A4, A6, FUNCT_7:31
.= (Exec (I,s)) . x by A1, A6, A7, ZFMISC_1:def 10 ; :: thesis: verum

end;

suppose x <> o ; :: thesis: ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x

hence ((Exec (I,s)) +* (o,a)) . x = (Exec (I,s)) . x by FUNCT_7:32; :: thesis: verum

end;

end;

end;

dom ((Exec (I,s)) +* (o,a)) = the carrier of A by PARTFUN1:def 2;
hence contradiction by A2, A3, A4, A5, FUNCT_1:2; :: thesis: verum