let D1, D2 be set ; :: thesis: for f1 being FinSequence of D1 *
for f2 being FinSequence of D2 *
for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 & j1 = j2 )
let f1 be FinSequence of D1 * ; :: thesis: for f2 being FinSequence of D2 *
for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 & j1 = j2 )
let f2 be FinSequence of D2 * ; :: thesis: for i1, i2, j1, j2 being Element of NAT st i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 holds
( i1 = i2 & j1 = j2 )
let i1, i2, j1, j2 be Element of NAT ; :: thesis: ( i1 in dom f1 & i2 in dom f2 & j1 in dom (f1 . i1) & j2 in dom (f2 . i2) & Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 implies ( i1 = i2 & j1 = j2 ) )
assume that
A1: i1 in dom f1 and
A2: i2 in dom f2 and
A3: j1 in dom (f1 . i1) and
A4: j2 in dom (f2 . i2) and
A5: ( Card f1 = Card f2 & (Sum ((Card f1) | (i1 -' 1))) + j1 = (Sum ((Card f2) | (i2 -' 1))) + j2 ) ; :: thesis: ( i1 = i2 & j1 = j2 )
A6: ( j1 >= 1 & j2 >= 1 ) by A3, A4, FINSEQ_3:25;
A7: 1 <= i1 by A1, FINSEQ_3:25;
then A8: i1 - 1 >= 0 by XREAL_1:48;
j1 <= len (f1 . i1) by A3, FINSEQ_3:25;
then j1 <= (Card f1) . i1 by A1, CARD_3:def 2;
then A9: j1 <= (Card f1) . ((i1 -' 1) + 1) by A7, XREAL_1:235;
A10: 1 <= i2 by A2, FINSEQ_3:25;
then A11: i2 - 1 >= 0 by XREAL_1:48;
dom (Card f2) = dom f2 by CARD_3:def 2;
then A12: len (Card f2) = len f2 by FINSEQ_3:29;
dom (Card f1) = dom f1 by CARD_3:def 2;
then A13: len (Card f1) = len f1 by FINSEQ_3:29;
i1 <= len f1 by A1, FINSEQ_3:25;
then i1 < (len f1) + 1 by NAT_1:13;
then i1 - 1 < ((len f1) + 1) - 1 by XREAL_1:9;
then A14: i1 -' 1 < len (Card f1) by A13, A8, XREAL_0:def 2;
j2 <= len (f2 . i2) by A4, FINSEQ_3:25;
then j2 <= (Card f2) . i2 by A2, CARD_3:def 2;
then A15: j2 <= (Card f2) . ((i2 -' 1) + 1) by A10, XREAL_1:235;
i2 <= len f2 by A2, FINSEQ_3:25;
then i2 < (len f2) + 1 by NAT_1:13;
then i2 - 1 < ((len f2) + 1) - 1 by XREAL_1:9;
then i2 -' 1 < len (Card f2) by A12, A11, XREAL_0:def 2;
then i1 -' 1 = i2 -' 1 by A5, A14, A6, A9, A15, Th20;
then i1 - 1 = i2 -' 1 by A8, XREAL_0:def 2;
then i1 - 1 = i2 - 1 by A11, XREAL_0:def 2;
hence ( i1 = i2 & j1 = j2 ) by A5, A14, A6, A9, A15, Th20; :: thesis: verum