let N be with_non-empty_elements set ; :: thesis: for IL being non empty set
for A being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,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 IL be non empty set ; :: thesis: for A being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,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 stored-program IC-Ins-separated definite AMI-Struct of IL,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 Th2;
then s . o = a by A1, YELLOW_8:def 1;
then A3: Exec I,(s +* o,a) = Exec I,s by FUNCT_7:37;
A4: dom ((Exec I,s) +* o,a) = the carrier of A by AMI_1:79;
A5: dom (Exec I,s) = the carrier of A by AMI_1:79;
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 Th2;
thus ((Exec I,s) +* o,a) . x = a by A5, A6, FUNCT_7:33
.= (Exec I,s) . x by A1, A6, A7, YELLOW_8:def 1 ; :: 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:34; :: thesis: verum

end;

end;

end;

hence contradiction by A2, A3, A4, A5, FUNCT_1:9; :: thesis: verum