let i1, i2 be SetSequence of Omega; :: thesis: ( ( for n being Element of NAT holds i1 . n = X /\ (f . n) ) & ( for n being Element of NAT holds i2 . n = X /\ (f . n) ) implies i1 = i2 )
assume A2: for n being Element of NAT holds i1 . n = X /\ (f . n) ; :: thesis: ( ex n being Element of NAT st not i2 . n = X /\ (f . n) or i1 = i2 )
assume A3: for n being Element of NAT holds i2 . n = X /\ (f . n) ; :: thesis: i1 = i2

now

let n be Element of NAT ; :: thesis: i1 . n = i2 . n
( i1 . n = X /\ (f . n) & i2 . n = X /\ (f . n) ) by A2, A3;
hence i1 . n = i2 . n ; :: thesis: verum

end;

hence i1 = i2 by FUNCT_2:113; :: thesis: verum