A1: (SCM+FSA-Memory --> (INT * )) +* (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) = ((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) by FUNCT_4:15;
A2: rng (((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) c= {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT }

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) or y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT } )
A3: dom (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) = (dom SCM-OK ) \/ (dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) by FUNCT_4:def 1
.= (dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) \/ ((dom SCM-OK ) \ (dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )))) by XBOOLE_1:39 ;
assume y in rng (((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) ; :: thesis: y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT }
then consider z being set such that
A4: z in dom (((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) and
A5: (((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) . z = y by FUNCT_1:def 5;
dom (((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) = (dom (SCM+FSA-Memory --> (INT * ))) \/ (dom (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )))) by A1, FUNCT_4:def 1
.= ((dom (SCM+FSA-Memory --> (INT * ))) \ (dom (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))))) \/ (dom (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )))) by XBOOLE_1:39 ;
then A6: ( z in (dom (SCM+FSA-Memory --> (INT * ))) \ (dom (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )))) or z in dom (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) ) by A4, XBOOLE_0:def 3;

per cases ( z in (dom (SCM+FSA-Memory --> (INT * ))) \ (dom (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )))) or z in dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) or z in (dom SCM-OK ) \ (dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) ) by A3, A6, XBOOLE_0:def 3;

suppose A7: z in (dom (SCM+FSA-Memory --> (INT * ))) \ (dom (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )))) ; :: thesis: y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT }

then not z in dom (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) by XBOOLE_0:def 5;
then (SCM+FSA-Memory --> (INT * )) . z = y by A1, A5, FUNCT_4:12;
then A8: y in rng (SCM+FSA-Memory --> (INT * )) by A7, FUNCT_1:def 5;
( {(INT * )} c= {INT ,(INT * )} & rng (SCM+FSA-Memory --> (INT * )) c= {(INT * )} ) by FUNCOP_1:19, ZFMISC_1:12;
then rng (SCM+FSA-Memory --> (INT * )) c= {INT ,(INT * )} by XBOOLE_1:1;
hence y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT } by A8, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A9: z in dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) ; :: thesis: y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT }

then ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) . z = y by A5, FUNCT_4:14;
then A10: y in rng ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) by A9, FUNCT_1:def 5;
rng ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) c= rng (SCM-Instr .--> SCM+FSA-Instr ) by RELAT_1:45;
then A11: rng ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) c= {SCM+FSA-Instr } by FUNCOP_1:14;
{SCM+FSA-Instr } c= {SCM+FSA-Instr ,NAT } by ZFMISC_1:12;
then rng ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) c= {SCM+FSA-Instr ,NAT } by A11, XBOOLE_1:1;
hence y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT } by A10, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A12: z in (dom SCM-OK ) \ (dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) ; :: thesis: y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT }

then A13: not z in dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) by XBOOLE_0:def 5;
z in (dom SCM-OK ) \/ (dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) by A12, XBOOLE_0:def 3;
then z in dom (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) by FUNCT_4:def 1;
then A14: y = (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) . z by A1, A5, FUNCT_4:14
.= SCM-OK . z by A13, FUNCT_4:12 ;
z in dom SCM-OK by A12;
then A15: z in SCM-Memory by FUNCT_2:def 1;
A16: dom SCM-OK = SCM-Memory by FUNCT_2:def 1;
rng (SCM-OK | NAT ) c= dom (SCM-Instr .--> SCM+FSA-Instr )

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in rng (SCM-OK | NAT ) or e in dom (SCM-Instr .--> SCM+FSA-Instr ) )
assume e in rng (SCM-OK | NAT ) ; :: thesis: e in dom (SCM-Instr .--> SCM+FSA-Instr )
then consider u being set such that
A17: u in dom (SCM-OK | NAT ) and
A18: (SCM-OK | NAT ) . u = e by FUNCT_1:def 5;
dom (SCM-OK | NAT ) c= NAT by RELAT_1:87;
then reconsider u = u as Element of NAT by A17;
e = SCM-OK . u by A17, A18, FUNCT_1:70
.= SCM-Instr by AMI_2:11 ;
then e in {SCM-Instr } by TARSKI:def 1;
hence e in dom (SCM-Instr .--> SCM+FSA-Instr ) by FUNCOP_1:19; :: thesis: verum

end;

then dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) = dom (SCM-OK | NAT ) by RELAT_1:46
.= NAT by A16, RELAT_1:91 ;
then not z in NAT by A12, XBOOLE_0:def 5;
then z in {NAT } \/ SCM-Data-Loc by A15, XBOOLE_0:def 3;
then A19: ( z in {NAT } or z in SCM-Data-Loc ) by XBOOLE_0:def 3;

now

per cases ( z = NAT or z in SCM-Data-Loc ) by A19, TARSKI:def 1;

suppose z = NAT ; :: thesis: y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT }

then y = NAT by A14, AMI_2:7, AMI_2:30;
then y in {SCM+FSA-Instr ,NAT } by TARSKI:def 2;
hence y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT } by XBOOLE_0:def 3; :: thesis: verum

end;

suppose z in SCM-Data-Loc ; :: thesis: y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT }

then y = INT by A14, AMI_2:10;
then y in {INT ,(INT * )} by TARSKI:def 2;
hence y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT } by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT } ; :: thesis: verum

end;

end;

end;

A20: dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) c= dom (SCM-OK | NAT ) by RELAT_1:44;
( dom SCM-OK c= SCM+FSA-Memory & dom (SCM-OK | NAT ) c= dom SCM-OK ) by Th1, FUNCT_2:def 1, RELAT_1:89;
then A21: dom (SCM-OK | NAT ) c= SCM+FSA-Memory by XBOOLE_1:1;
dom ((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) = (dom (SCM+FSA-Memory --> (INT * ))) \/ (dom SCM-OK ) by FUNCT_4:def 1
.= SCM+FSA-Memory \/ (dom SCM-OK ) by FUNCOP_1:19
.= SCM+FSA-Memory \/ SCM-Memory by FUNCT_2:def 1
.= SCM+FSA-Memory by XBOOLE_1:7, XBOOLE_1:12 ;
then dom (((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) = SCM+FSA-Memory \/ (dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) by FUNCT_4:def 1
.= SCM+FSA-Memory by A21, A20, XBOOLE_1:1, XBOOLE_1:12 ;
hence ((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) is Function of SCM+FSA-Memory ,({INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT }) by A2, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum