A1: dom SCM-OK c= SCM+FSA-Memory by Th1, FUNCT_2:def 1;
dom (SCM-OK | NAT ) c= dom SCM-OK by RELAT_1:89;
then A2: dom (SCM-OK | NAT ) c= SCM+FSA-Memory by A1, XBOOLE_1:1;
A3: dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) c= dom (SCM-OK | NAT ) by RELAT_1:44;
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 A4: 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 A2, A3, XBOOLE_1:1, XBOOLE_1:12 ;
A5: (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;
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 } )
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
A6: z in dom (((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) and
A7: (((SCM+FSA-Memory --> (INT * )) +* SCM-OK ) +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) . z = y by FUNCT_1:def 5;
A8: 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 A5, 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 ;
A9: 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 ;
A10: ( 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 A6, A8, 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 A9, A10, XBOOLE_0:def 3;

suppose A11: 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 A5, A7, FUNCT_4:12;
then A12: y in rng (SCM+FSA-Memory --> (INT * )) by A11, FUNCT_1:def 5;
A13: {(INT * )} c= {INT ,(INT * )} by ZFMISC_1:12;
rng (SCM+FSA-Memory --> (INT * )) c= {(INT * )} by FUNCOP_1:19;
then rng (SCM+FSA-Memory --> (INT * )) c= {INT ,(INT * )} by A13, XBOOLE_1:1;
hence y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT } by A12, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A14: 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 A7, FUNCT_4:14;
then A15: y in rng ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) by A14, 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 A16: 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 A16, XBOOLE_1:1;
hence y in {INT ,(INT * )} \/ {SCM+FSA-Instr ,NAT } by A15, XBOOLE_0:def 3; :: thesis: verum

end;

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

then A18: not z in dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT )) by XBOOLE_0:def 5;
A19: z in dom SCM-OK by A17;
z in (dom SCM-OK ) \/ (dom ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) by A17, XBOOLE_0:def 3;
then z in dom (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) by FUNCT_4:def 1;
then A20: y = (SCM-OK +* ((SCM-Instr .--> SCM+FSA-Instr ) * (SCM-OK | NAT ))) . z by A5, A7, FUNCT_4:14
.= SCM-OK . z by A18, FUNCT_4:12 ;
A21: z in SCM-Memory by A19, FUNCT_2:def 1;
A22: 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
A23: u in dom (SCM-OK | NAT ) and
A24: (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 A23;
e = SCM-OK . u by A23, A24, 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 A22, RELAT_1:91 ;
then not z in NAT by A17, XBOOLE_0:def 5;
then z in {(IC SCM )} \/ SCM-Data-Loc by A21, AMI_3:def 1, AMI_5:23, XBOOLE_0:def 3;
then A25: ( z in {(IC SCM )} or z in SCM-Data-Loc ) by XBOOLE_0:def 3;

now

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

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

then y = NAT by A20, 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 A20, 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;

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 A4, FUNCT_2:def 1, RELSET_1:11; :: thesis: verum