defpred S₁[ object , object ] means ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & $1 = (fsloc 0) .--> t & $2 = (fsloc 0) .--> u );
A1: for x, y1, y2 being object st S₁[x,y1] & S₁[x,y2] holds
y1 = y2

proof

let p, q1, q2 be object ; :: thesis: ( S₁[p,q1] & S₁[p,q2] implies q1 = q2 )
given t1 being FinSequence of INT , u1 being FinSequence of REAL such that A2: t1,u1 are_fiberwise_equipotent and
u1 is FinSequence of INT and
A3: u1 is non-increasing and
A4: p = (fsloc 0) .--> t1 and
A5: q1 = (fsloc 0) .--> u1 ; :: thesis: ( not S₁[p,q2] or q1 = q2 )
given t2 being FinSequence of INT , u2 being FinSequence of REAL such that A6: t2,u2 are_fiberwise_equipotent and
u2 is FinSequence of INT and
A7: u2 is non-increasing and
A8: p = (fsloc 0) .--> t2 and
A9: q2 = (fsloc 0) .--> u2 ; :: thesis: q1 = q2
t1 = ((fsloc 0) .--> t1) . (fsloc 0) by FUNCOP_1:72
.= t2 by A4, A8, FUNCOP_1:72 ;
hence q1 = q2 by A2, A3, A5, A6, A7, A9, CLASSES1:76, RFINSEQ:23; :: thesis: verum

end;

consider f being Function such that
A10: for p, q being object holds
( [p,q] in f iff ( p in FinPartSt SCM+FSA & S₁[p,q] ) ) from FUNCT_1:sch 1(A1);
A11: dom f c= FinPartSt SCM+FSA

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in dom f or e in FinPartSt SCM+FSA )
assume e in dom f ; :: thesis: e in FinPartSt SCM+FSA
then [e,(f . e)] in f by FUNCT_1:1;
hence e in FinPartSt SCM+FSA by A10; :: thesis: verum

end;

rng f c= FinPartSt SCM+FSA

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in rng f or q in FinPartSt SCM+FSA )
assume q in rng f ; :: thesis: q in FinPartSt SCM+FSA
then consider p being object such that
A12: [p,q] in f by XTUPLE_0:def 13;
consider t being FinSequence of INT , u being FinSequence of REAL such that
t,u are_fiberwise_equipotent and
A13: u is FinSequence of INT and
u is non-increasing and
p = (fsloc 0) .--> t and
A14: q = (fsloc 0) .--> u by A10, A12;
reconsider u = u as FinSequence of INT by A13;
(fsloc 0) .--> u is FinPartState of SCM+FSA ;
hence q in FinPartSt SCM+FSA by A14, MEMSTR_0:75; :: thesis: verum

end;

then reconsider f = f as PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) by A11, RELSET_1:4;
take f ; :: thesis: for p, q being FinPartState of SCM+FSA holds
( [p,q] in f iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) )
let p, q be FinPartState of SCM+FSA; :: thesis: ( [p,q] in f iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) )
thus ( [p,q] in f implies ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) by A10; :: thesis: ( ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) implies [p,q] in f )
given t being FinSequence of INT , u being FinSequence of REAL such that A15: t,u are_fiberwise_equipotent and
A16: u is FinSequence of INT and
A17: u is non-increasing and
A18: p = (fsloc 0) .--> t and
A19: q = (fsloc 0) .--> u ; :: thesis: [p,q] in f
p in FinPartSt SCM+FSA by MEMSTR_0:75;
hence [p,q] in f by A10, A15, A16, A17, A18, A19; :: thesis: verum