let m, n be Nat; 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 ; 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); ( ( 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
; 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 )
;
hence
F1 = F2
by P1, P2, FINSEQ_1:14; verum