let g, h be FinSequence of NAT ; :: thesis: ( dom g = Seg (card S) & ( for n being Nat st n in dom g holds

g . n = (len s) * ((FDprobSEQ s) . n) ) & dom h = Seg (card S) & ( for n being Nat st n in dom h holds

h . n = (len s) * ((FDprobSEQ s) . n) ) implies g = h )

assume that

A7: dom g = Seg (card S) and

A8: for n being Nat st n in dom g holds

g . n = (len s) * ((FDprobSEQ s) . n) ; :: thesis: ( not dom h = Seg (card S) or ex n being Nat st

( n in dom h & not h . n = (len s) * ((FDprobSEQ s) . n) ) or g = h )

assume that

A9: dom h = Seg (card S) and

A10: for n being Nat st n in dom h holds

h . n = (len s) * ((FDprobSEQ s) . n) ; :: thesis: g = h

.= len h by A9, FINSEQ_1:def 3 ;

hence g = h by A11, FINSEQ_2:9; :: thesis: verum

g . n = (len s) * ((FDprobSEQ s) . n) ) & dom h = Seg (card S) & ( for n being Nat st n in dom h holds

h . n = (len s) * ((FDprobSEQ s) . n) ) implies g = h )

assume that

A7: dom g = Seg (card S) and

A8: for n being Nat st n in dom g holds

g . n = (len s) * ((FDprobSEQ s) . n) ; :: thesis: ( not dom h = Seg (card S) or ex n being Nat st

( n in dom h & not h . n = (len s) * ((FDprobSEQ s) . n) ) or g = h )

assume that

A9: dom h = Seg (card S) and

A10: for n being Nat st n in dom h holds

h . n = (len s) * ((FDprobSEQ s) . n) ; :: thesis: g = h

A11: now :: thesis: for n being Nat st n in dom g holds

g . n = h . n

len g =
card S
by A7, FINSEQ_1:def 3
g . n = h . n

let n be Nat; :: thesis: ( n in dom g implies g . n = h . n )

assume A12: n in dom g ; :: thesis: g . n = h . n

hence g . n = (len s) * ((FDprobSEQ s) . n) by A8

.= h . n by A7, A9, A10, A12 ;

:: thesis: verum

end;assume A12: n in dom g ; :: thesis: g . n = h . n

hence g . n = (len s) * ((FDprobSEQ s) . n) by A8

.= h . n by A7, A9, A10, A12 ;

:: thesis: verum

.= len h by A9, FINSEQ_1:def 3 ;

hence g = h by A11, FINSEQ_2:9; :: thesis: verum