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