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