let f1, f2 be SetSequence of El_Filtration (t,MyFunc); :: thesis: ( ( for n being Nat holds f1 . n = Sigma_tauhelp2 (tau,A,n,t) ) & ( for n being Nat holds f2 . n = Sigma_tauhelp2 (tau,A,n,t) ) implies f1 = f2 )
assume that
A1: for d being Nat holds f1 . d = Sigma_tauhelp2 (tau,A,d,t) and
A2: for d being Nat holds f2 . d = Sigma_tauhelp2 (tau,A,d,t) ; :: thesis: f1 = f2
for d being Nat holds f1 . d = f2 . d
proof
let d be Nat; :: thesis: f1 . d = f2 . d
f1 . d = Sigma_tauhelp2 (tau,A,d,t) by A1;
hence f1 . d = f2 . d by A2; :: thesis: verum
end;
hence f1 = f2 ; :: thesis: verum