A1:
SCM+FSA-Memory c= (union {INT ,(INT * )}) \/ SCM+FSA-Memory
by XBOOLE_1:7;
A2:
{ [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } c= [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } or x in [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):] )
assume
x in { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} }
;
:: thesis: x in [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):]
then consider J being
Element of
Segm 13,
c,
b being
Element of
SCM+FSA-Data-Loc ,
f being
Element of
SCM+FSA-Data*-Loc such that A3:
(
x = [J,<*c,f,b*>] &
J in {9,10} )
;
reconsider c =
c,
f =
f,
b =
b as
Element of
(union {INT ,(INT * )}) \/ SCM+FSA-Memory by A1, TARSKI:def 3;
<*c,f,b*> in ((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) *
by FINSEQ_1:def 11;
hence
x in [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):]
by A3, ZFMISC_1:106;
:: thesis: verum
end;
A4:
{ [K,<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } c= [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { [K,<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } or x in [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):] )
assume
x in { [K,<*c,f*>] where K is Element of Segm 13, c is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : K in {11,12} }
;
:: thesis: x in [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):]
then consider K being
Element of
Segm 13,
c being
Element of
SCM+FSA-Data-Loc ,
f being
Element of
SCM+FSA-Data*-Loc such that A5:
(
x = [K,<*c,f*>] &
K in {11,12} )
;
reconsider c =
c,
f =
f as
Element of
(union {INT ,(INT * )}) \/ SCM+FSA-Memory by A1, TARSKI:def 3;
<*c,f*> in ((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) *
by FINSEQ_1:def 11;
hence
x in [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):]
by A5, ZFMISC_1:106;
:: thesis: verum
end;
union {INT } c= union {INT ,(INT * )}
by ZFMISC_1:12, ZFMISC_1:95;
then
(union {INT }) \/ SCM-Memory c= (union {INT ,(INT * )}) \/ SCM+FSA-Memory
by Th1, XBOOLE_1:13;
then
((union {INT }) \/ SCM-Memory ) * c= ((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) *
by FINSEQ_1:83;
then
[:NAT ,(((union {INT }) \/ SCM-Memory ) * ):] c= [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):]
by ZFMISC_1:119;
then
SCM-Instr c= [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):]
by XBOOLE_1:1;
then
SCM-Instr \/ { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } c= [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):]
by A2, XBOOLE_1:8;
hence
(SCM-Instr \/ { [J,<*c,f,b*>] where J is Element of Segm 13, c, b is Element of SCM+FSA-Data-Loc , f is Element of SCM+FSA-Data*-Loc : J in {9,10} } ) \/ { [K,<*c1,f1*>] where K is Element of Segm 13, c1 is Element of SCM+FSA-Data-Loc , f1 is Element of SCM+FSA-Data*-Loc : K in {11,12} } is Subset of [:NAT ,(((union {INT ,(INT * )}) \/ SCM+FSA-Memory ) * ):]
by A4, XBOOLE_1:8; :: thesis: verum