let f1, f2 be SetSequence of REAL; :: thesis: ( ( for n being Nat holds f1 . n = {((pm * k) * ((n + 1) "))} ) & ( for n being Nat holds f2 . n = {((pm * k) * ((n + 1) "))} ) implies f1 = f2 )
assume A1: for d being Nat holds f1 . d = {((pm * k) * ((d + 1) "))} ; :: thesis: ( ex n being Nat st not f2 . n = {((pm * k) * ((n + 1) "))} or f1 = f2 )
assume A2: for d being Nat holds f2 . d = {((pm * k) * ((d + 1) "))} ; :: thesis: f1 = f2
for d being Nat holds f1 . d = f2 . d

proof

let d be Nat; :: thesis: f1 . d = f2 . d
f2 . d = {((pm * k) * ((d + 1) "))} by A2;
hence f1 . d = f2 . d by A1; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum