defpred S1[ 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 S1[x,y1] & S1[x,y2] holds
y1 = y2
proof
let p,
q1,
q2 be
object ;
( S1[p,q1] & S1[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
;
( not S1[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
;
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;
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 & S1[p,q] ) )
from FUNCT_1:sch 1(A1);
A11:
dom f c= FinPartSt SCM+FSA
rng f c= FinPartSt SCM+FSA
then reconsider f = f as PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) by A11, RELSET_1:4;
take
f
; 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; ( [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; ( 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
; [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; verum