A2: rng ((SCM+FSA-Memory --> (INT *)) +* SCM-OK) c= {INT,(INT *)} \/ {NAT}

proof

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

per cases ( z in (dom (SCM+FSA-Memory --> (INT *))) \ (dom SCM-OK) or z in dom SCM-OK ) by A6;

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

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

end;

suppose A12: z in dom SCM-OK ; :: thesis: y in {INT,(INT *)} \/ {NAT}

z in dom SCM-OK by A12;
then z in dom SCM-OK ;
then A14: y = SCM-OK . z by A5, FUNCT_4:13
.= SCM-OK . z ;
z in dom SCM-OK by A12;
then A15: z in SCM-Memory by FUNCT_2:def 1;
z in {NAT} \/ SCM-Data-Loc by A15;
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 *)} \/ {NAT}

then y = NAT by A14, AMI_2:6, AMI_2:22;
then y in {NAT} by TARSKI:def 1;
hence y in {INT,(INT *)} \/ {NAT} by XBOOLE_0:def 3; :: thesis: verum

end;

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

then y = INT by A14, AMI_2:8;
then y in {INT,(INT *)} by TARSKI:def 2;
hence y in {INT,(INT *)} \/ {NAT} by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence y in {INT,(INT *)} \/ {NAT} ; :: thesis: verum

end;

end;

end;

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:13
.= 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+FSA-Memory
.= SCM+FSA-Memory ;
hence (SCM+FSA-Memory --> (INT *)) +* SCM-OK is Function of SCM+FSA-Memory,({INT,(INT *)} \/ {NAT}) by A2, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum