let m, n be Nat; :: thesis: for D being non empty set
for F1, F2 being Element of m -tuples_on (n -tuples_on D) st ( for i, j being Nat st i in Seg m & j in Seg n holds
(F1 . i) . j = (F2 . i) . j ) holds
F1 = F2
let D be non empty set ; :: thesis: for F1, F2 being Element of m -tuples_on (n -tuples_on D) st ( for i, j being Nat st i in Seg m & j in Seg n holds
(F1 . i) . j = (F2 . i) . j ) holds
F1 = F2
let F1, F2 be Element of m -tuples_on (n -tuples_on D); :: thesis: ( ( for i, j being Nat st i in Seg m & j in Seg n holds
(F1 . i) . j = (F2 . i) . j ) implies F1 = F2 )
assume AS: for i, j being Nat st i in Seg m & j in Seg n holds
(F1 . i) . j = (F2 . i) . j ; :: thesis: F1 = F2
F1 in m -tuples_on (n -tuples_on D) ;
then P1: ex s being Element of (n -tuples_on D) * st
( F1 = s & len s = m ) ;
F2 in m -tuples_on (n -tuples_on D) ;
then P2: ex s being Element of (n -tuples_on D) * st
( F2 = s & len s = m ) ;
now :: thesis: for i being Nat st 1 <= i & i <= len F1 holds
F1 . i = F2 . i
let i be Nat; :: thesis: ( 1 <= i & i <= len F1 implies F1 . i = F2 . i )
assume ( 1 <= i & i <= len F1 ) ; :: thesis: F1 . i = F2 . i
then P4: i in Seg m by P1;
then i in dom F1 by FINSEQ_1:def 3, P1;
then F1 . i in rng F1 by FUNCT_1:3;
then F1 . i in n -tuples_on D ;
then P6: ex s being Element of D * st
( F1 . i = s & len s = n ) ;
then reconsider F1i = F1 . i as Element of D * ;
i in dom F2 by FINSEQ_1:def 3, P2, P4;
then F2 . i in rng F2 by FUNCT_1:3;
then F2 . i in n -tuples_on D ;
then R6: ex s being Element of D * st
( F2 . i = s & len s = n ) ;
then reconsider F2i = F2 . i as Element of D * ;
now :: thesis: for j being Nat st 1 <= j & j <= len F1i holds
F1i . j = F2i . j
let j be Nat; :: thesis: ( 1 <= j & j <= len F1i implies F1i . j = F2i . j )
assume ( 1 <= j & j <= len F1i ) ; :: thesis: F1i . j = F2i . j
then j in Seg n by P6;
hence F1i . j = F2i . j by AS, P4; :: thesis: verum
end;
hence F1 . i = F2 . i by P6, R6, FINSEQ_1:14; :: thesis: verum
end;
hence F1 = F2 by P1, P2, FINSEQ_1:14; :: thesis: verum