A1: rng ((SCM+FSA-Memory --> 2) +* SCM-OK) c= 3

proof

rng (SCM+FSA-Memory --> 2) = {2} by FUNCOP_1:8;
then A2: rng ((SCM+FSA-Memory --> 2) +* SCM-OK) c= {2} \/ (rng SCM-OK) by FUNCT_4:17;
rng SCM-OK c= Segm 2 by RELAT_1:def 19;
then {2} \/ (rng SCM-OK) c= 2 \/ {2} by XBOOLE_1:9;
then rng ((SCM+FSA-Memory --> 2) +* SCM-OK) c= 2 \/ {2} by A2;
then rng ((SCM+FSA-Memory --> 2) +* SCM-OK) c= succ 2 ;
hence rng ((SCM+FSA-Memory --> 2) +* SCM-OK) c= 3 ; :: thesis: verum

end;

dom ((SCM+FSA-Memory --> 2) +* SCM-OK) = (dom (SCM+FSA-Memory --> 2)) \/ (dom SCM-OK) by FUNCT_4:def 1
.= SCM+FSA-Memory \/ (dom SCM-OK)
.= 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 --> 2) +* SCM-OK) = SCM+FSA-Memory
.= SCM+FSA-Memory ;
hence (SCM+FSA-Memory --> 2) +* SCM-OK is Function of SCM+FSA-Memory,(Segm 3) by A1, FUNCT_2:def 1, RELSET_1:4; :: thesis: verum