let s be State of SCM+FSA ; :: thesis: for t being FinSequence of INT st (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> t) c= s holds
ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result s) . (fsloc 0 ) = u )
let t be FinSequence of INT ; :: thesis: ( (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> t) c= s implies ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result s) . (fsloc 0 ) = u ) )
set Ba = Bubble-Sort-Algorithm ;
set p = Initialized Bubble-Sort-Algorithm ;
set x = (fsloc 0 ) .--> t;
set z = (IExec (bubble-sort (fsloc 0 )),s) . (fsloc 0 );
assume A1: (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> t) c= s ; :: thesis: ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is non-increasing & u is FinSequence of INT & (Result s) . (fsloc 0 ) = u )
dom ((fsloc 0 ) .--> t) = {(fsloc 0 )} by FUNCOP_1:19;
then A2: fsloc 0 in dom ((fsloc 0 ) .--> t) by TARSKI:def 1;
then fsloc 0 in dom ((Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> t)) by FUNCT_4:13;
then A3: s . (fsloc 0 ) = ((Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> t)) . (fsloc 0 ) by A1, GRFUNC_1:8
.= ((fsloc 0 ) .--> t) . (fsloc 0 ) by A2, FUNCT_4:14
.= t by FUNCOP_1:87 ;
A4: ( s . (fsloc 0 ),(IExec (bubble-sort (fsloc 0 )),s) . (fsloc 0 ) are_fiberwise_equipotent & ( for i, j being Element of NAT st i >= 1 & j <= len (s . (fsloc 0 )) & i < j holds
for x1, x2 being Integer st x1 = ((IExec (bubble-sort (fsloc 0 )),s) . (fsloc 0 )) . i & x2 = ((IExec (bubble-sort (fsloc 0 )),s) . (fsloc 0 )) . j holds
x1 >= x2 ) ) by Th65;
reconsider u = (IExec (bubble-sort (fsloc 0 )),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 s) . (fsloc 0 ) = u )
thus t,u are_fiberwise_equipotent by A3, Th65; :: thesis: ( u is non-increasing & u is FinSequence of INT & (Result s) . (fsloc 0 ) = u )
A5: dom (s . (fsloc 0 )) = dom u by A4, 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 A6: ( i in dom u & j in dom u & i < j ) ; :: thesis: u . i >= u . j
then A7: i >= 1 by FINSEQ_3:27;
A8: j <= len (s . (fsloc 0 )) by A5, A6, FINSEQ_3:27;
reconsider y1 = ((IExec (bubble-sort (fsloc 0 )),s) . (fsloc 0 )) . i as Integer ;
reconsider y2 = ((IExec (bubble-sort (fsloc 0 )),s) . (fsloc 0 )) . j as Integer ;
y1 >= y2 by A6, A7, A8, Th65;
hence u . i >= u . j ; :: thesis: verum

end;

hence u is non-increasing by RFINSEQ:32; :: thesis: ( u is FinSequence of INT & (Result s) . (fsloc 0 ) = u )
thus u is FinSequence of INT ; :: thesis: (Result s) . (fsloc 0 ) = u
dom (Initialized Bubble-Sort-Algorithm ) misses dom ((fsloc 0 ) .--> t) by Th46;
then Initialized Bubble-Sort-Algorithm c= (Initialized Bubble-Sort-Algorithm ) +* ((fsloc 0 ) .--> t) by FUNCT_4:33;
then Initialized Bubble-Sort-Algorithm c= s by A1, XBOOLE_1:1;
then s = s +* (Initialized Bubble-Sort-Algorithm ) by FUNCT_4:79;
hence (Result s) . (fsloc 0 ) = u by Th57; :: thesis: verum