reconsider C = <%R%> as non empty 0 -based array ;
take C ; :: thesis: ( C . (base- C) = R & ( for a being Ordinal st a in dom C holds
C . a is array of O ) & ( for a being Ordinal st a in dom C & succ a in dom C holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) ) )
A1: ( dom C = 1 & 0 in Segm 1 ) by AFINSQ_1:def 4, NAT_1:44;
then base- C = 0 by Def4;
hence C . (base- C) = R ; :: thesis: ( ( for a being Ordinal st a in dom C holds
C . a is array of O ) & ( for a being Ordinal st a in dom C & succ a in dom C holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) ) )
hereby :: thesis: for a being Ordinal st a in dom C & succ a in dom C holds
ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) )
let a be Ordinal; :: thesis: ( a in dom C implies C . a is array of O )
assume a in dom C ; :: thesis: C . a is array of O
then a = 0 by A1, ORDINAL3:15, TARSKI:def 1;
hence C . a is array of O ; :: thesis: verum
end;
let a be Ordinal; :: thesis: ( a in dom C & succ a in dom C implies ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) )
assume ( a in dom C & succ a in dom C ) ; :: thesis: ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) )
hence ex R being array of O ex x, y being set st
( [x,y] in inversions R & C . a = R & C . (succ a) = Swap (R,x,y) ) by A1, ORDINAL3:15, TARSKI:def 1; :: thesis: verum