A1:
SCM-Memory c= (union {the carrier of S}) \/ SCM-Memory
by XBOOLE_1:7;
A2:
{ [I,<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } c= [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { [I,<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } or x in [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):] )
assume
x in { [I,<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} }
;
:: thesis: x in [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
then consider I being
Element of
Segm 8,
d1,
d2 being
Element of
SCM-Data-Loc such that A3:
x = [I,<*d1,d2*>]
and
I in {1,2,3,4}
;
reconsider d1 =
d1,
d2 =
d2 as
Element of
(union {the carrier of S}) \/ SCM-Memory by A1, TARSKI:def 3;
<*d1,d2*> in ((union {the carrier of S}) \/ SCM-Memory ) *
by FINSEQ_1:def 11;
hence
x in [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
by A3, ZFMISC_1:106;
:: thesis: verum
end;
A4:
{ [6,<*i1*>] where i1 is Element of NAT : verum } c= [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
A6:
{ [7,<*i2,d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum } c= [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { [7,<*i2,d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum } or x in [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):] )
assume
x in { [7,<*i2,d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum }
;
:: thesis: x in [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
then consider i2 being
Element of
NAT ,
d3 being
Element of
SCM-Data-Loc such that A7:
x = [7,<*i2,d3*>]
and
verum
;
reconsider i2 =
i2,
d3 =
d3 as
Element of
(union {the carrier of S}) \/ SCM-Memory by A1, TARSKI:def 3;
<*i2,d3*> in ((union {the carrier of S}) \/ SCM-Memory ) *
by FINSEQ_1:def 11;
hence
x in [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
by A7, ZFMISC_1:106;
:: thesis: verum
end;
A8:
{ [5,<*d4,r*>] where d4 is Element of SCM-Data-Loc , r is Element of S : verum } c= [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in { [5,<*d4,r*>] where d4 is Element of SCM-Data-Loc , r is Element of S : verum } or x in [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):] )
assume
x in { [5,<*d4,r*>] where d4 is Element of SCM-Data-Loc , r is Element of S : verum }
;
:: thesis: x in [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
then consider d4 being
Element of
SCM-Data-Loc such that A9:
ex
r being
Element of
S st
x = [5,<*d4,r*>]
;
consider r being
Element of
S such that A10:
x = [5,<*d4,r*>]
and
verum
by A9;
union {the carrier of S} = the
carrier of
S
by ZFMISC_1:31;
then
the
carrier of
S c= (union {the carrier of S}) \/ SCM-Memory
by XBOOLE_1:7;
then reconsider d4 =
d4,
r =
r as
Element of
(union {the carrier of S}) \/ SCM-Memory by A1, TARSKI:def 3;
<*d4,r*> in ((union {the carrier of S}) \/ SCM-Memory ) *
by FINSEQ_1:def 11;
hence
x in [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
by A10, ZFMISC_1:106;
:: thesis: verum
end;
( 0 in Segm 8 & {} in ((union {the carrier of S}) \/ SCM-Memory ) * )
by FINSEQ_1:66, GR_CY_1:10;
then
[0 ,{} ] in [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
by ZFMISC_1:106;
then
{[0 ,{} ]} c= [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
by ZFMISC_1:37;
then
{[0 ,{} ]} \/ { [I,<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } c= [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
by A2, XBOOLE_1:8;
then
({[0 ,{} ]} \/ { [I,<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i1*>] where i1 is Element of NAT : verum } c= [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
by A4, XBOOLE_1:8;
then
(({[0 ,{} ]} \/ { [I,<*d1,d2*>] where I is Element of Segm 8, d1, d2 is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i1*>] where i1 is Element of NAT : verum } ) \/ { [7,<*i2,d3*>] where i2 is Element of NAT , d3 is Element of SCM-Data-Loc : verum } c= [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
by A6, XBOOLE_1:8;
hence
((({[0 ,{} ]} \/ { [I,<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>] where i is Element of NAT : verum } ) \/ { [7,<*i,a*>] where i is Element of NAT , a is Element of SCM-Data-Loc : verum } ) \/ { [5,<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } is Subset of [:NAT ,(((union {the carrier of S}) \/ SCM-Memory ) * ):]
by A8, XBOOLE_1:8; :: thesis: verum