set f = Sorting-Function ;
let p be set ; :: thesis: ( p in dom Sorting-Function iff ex t being FinSequence of INT st p = (fsloc 0) .--> t )
hereby :: thesis: ( ex t being FinSequence of INT st p = (fsloc 0) .--> t implies p in dom Sorting-Function )
set q = Sorting-Function . p;
assume A1: p in dom Sorting-Function ; :: thesis: ex t being FinSequence of INT st p = (fsloc 0) .--> t
then A2: [p,(Sorting-Function . p)] in Sorting-Function by FUNCT_1:1;
dom Sorting-Function c= FinPartSt SCM+FSA by RELAT_1:def 18;
then A3: p is FinPartState of SCM+FSA by A1, MEMSTR_0:76;
Sorting-Function . p in FinPartSt SCM+FSA by A1, PARTFUN1:4;
then Sorting-Function . p is FinPartState of SCM+FSA by MEMSTR_0:76;
then consider t being FinSequence of INT , u being FinSequence of REAL such that
t,u are_fiberwise_equipotent and
u is FinSequence of INT and
u is non-increasing and
A4: p = (fsloc 0) .--> t and
Sorting-Function . p = (fsloc 0) .--> u by A2, A3, Def7;
take t = t; :: thesis: p = (fsloc 0) .--> t
thus p = (fsloc 0) .--> t by A4; :: thesis: verum
end;
given t being FinSequence of INT such that A5: p = (fsloc 0) .--> t ; :: thesis: p in dom Sorting-Function
consider u being FinSequence of REAL such that
A6: t,u are_fiberwise_equipotent and
A7: u is FinSequence of INT and
A8: u is non-increasing by RFINSEQ:33;
reconsider u1 = u as FinSequence of INT by A7;
set q = (fsloc 0) .--> u1;
[p,((fsloc 0) .--> u1)] in Sorting-Function by A5, A6, A8, Def7;
hence p in dom Sorting-Function by FUNCT_1:1; :: thesis: verum