let f1, f2 be sequence of D; :: thesis: ( ( for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & f1 . n = (s . k) . m ) ) & ( for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & f2 . n = (s . k) . m ) ) implies f1 = f2 )
assume that
A1: for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & f1 . n = (s . k) . m ) and
A2: for n being Nat ex k, m being Nat st
( m in dom (s . k) & ((((Partial_Sums (Length s)) . k) - (len (s . k))) + m) - 1 = n & f2 . n = (s . k) . m ) ; :: thesis: f1 = f2
for n being Element of NAT holds f1 . n = f2 . n

proof

let n be Element of NAT ; :: thesis: f1 . n = f2 . n
consider k1, m1 being Nat such that
A3: ( m1 in dom (s . k1) & ((((Partial_Sums (Length s)) . k1) - (len (s . k1))) + m1) - 1 = n & f1 . n = (s . k1) . m1 ) by A1;
consider k2, m2 being Nat such that
A4: ( m2 in dom (s . k2) & ((((Partial_Sums (Length s)) . k2) - (len (s . k2))) + m2) - 1 = n & f2 . n = (s . k2) . m2 ) by A2;
( m1 = m2 & k1 = k2 ) by A3, A4, Th10;
hence f1 . n = f2 . n by A3, A4; :: thesis: verum

end;

hence f1 = f2 by FUNCT_2:def 8; :: thesis: verum