let p be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: for s being State of SCM+FSA
for t being FinSequence of INT st (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s & Bubble-Sort-Algorithm c= p holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )
let s be State of SCM+FSA; :: thesis: for t being FinSequence of INT st (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s & Bubble-Sort-Algorithm c= p holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )
let t be FinSequence of INT ; :: thesis: ( (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s & Bubble-Sort-Algorithm c= p implies ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u ) )
set Ba = Bubble-Sort-Algorithm ;
set pp = Initialize ((intloc 0) .--> 1);
set x = (fsloc 0) .--> t;
set z = (IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0);
assume that
A1: (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) c= s and
A2: Bubble-Sort-Algorithm c= p ; :: thesis: ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )
A3: p +* Bubble-Sort-Algorithm = p by A2, FUNCT_4:103, FUNCT_4:104;
dom ((fsloc 0) .--> t) = {(fsloc 0)} by FUNCOP_1:19;
then A4: fsloc 0 in dom ((fsloc 0) .--> t) by TARSKI:def 1;
then fsloc 0 in dom ((Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t)) by FUNCT_4:13;
then A5: s . (fsloc 0) = ((Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t)) . (fsloc 0) by A1, GRFUNC_1:8
.= ((fsloc 0) .--> t) . (fsloc 0) by A4, FUNCT_4:14
.= t by FUNCOP_1:87 ;
A6: s . (fsloc 0),(IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0) are_fiberwise_equipotent by Th65;
reconsider u = (IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0) as FinSequence of REAL by FINSEQ_3:126;
take u ; :: thesis: ( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )
thus t,u are_fiberwise_equipotent by A5, Th65; :: thesis: ( u is non-increasing & u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )
A7: dom (s . (fsloc 0)) = dom u by A6, RFINSEQ:16;

now

let i, j be Element of NAT ; :: thesis: ( i in dom u & j in dom u & i < j implies u . i >= u . j )
assume that
A8: i in dom u and
A9: j in dom u and
A10: i < j ; :: thesis: u . i >= u . j
A11: i >= 1 by A8, FINSEQ_3:27;
A12: j <= len (s . (fsloc 0)) by A7, A9, FINSEQ_3:27;
reconsider y1 = ((IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0)) . i as Integer ;
reconsider y2 = ((IExec ((bubble-sort (fsloc 0)),p,s)) . (fsloc 0)) . j as Integer ;
thus u . i >= u . j by A10, A11, A12, Th65; :: thesis: verum

end;

hence u is non-increasing by RFINSEQ:32; :: thesis: ( u is FinSequence of INT & (Result (p,s)) . (fsloc 0) = u )
thus u is FinSequence of INT ; :: thesis: (Result (p,s)) . (fsloc 0) = u
Initialized Bubble-Sort-Algorithm = Bubble-Sort-Algorithm +* (Initialize ((intloc 0) .--> 1)) by SCMFSA6A:def 4;
then Initialize ((intloc 0) .--> 1) c= Initialized Bubble-Sort-Algorithm by FUNCT_4:26;
then xx: dom (Initialize ((intloc 0) .--> 1)) c= dom (Initialized Bubble-Sort-Algorithm) by RELAT_1:25;
dom (Initialized Bubble-Sort-Algorithm) misses dom ((fsloc 0) .--> t) by Th46;
then dom (Initialize ((intloc 0) .--> 1)) misses dom ((fsloc 0) .--> t) by xx, XBOOLE_1:63;
then Initialize ((intloc 0) .--> 1) c= (Initialize ((intloc 0) .--> 1)) +* ((fsloc 0) .--> t) by FUNCT_4:33;
then Initialize ((intloc 0) .--> 1) c= s by A1, XBOOLE_1:1;
then x: s = s +* (Initialize ((intloc 0) .--> 1)) by FUNCT_4:103, FUNCT_4:104;
(Result (p,(s +* (Initialize ((intloc 0) .--> 1))))) . (fsloc 0) = (IExec (Bubble-Sort-Algorithm,p,s)) . (fsloc 0) by Th57, A3;
hence (Result (p,s)) . (fsloc 0) = u by x; :: thesis: verum