let i1, i2 be SetSequence of Omega; :: thesis: ( ( for n being Nat holds i1 . n = disjointify g,n ) & ( for n being Nat holds i2 . n = disjointify g,n ) implies i1 = i2 )
assume A2: for n being Nat holds i1 . n = disjointify g,n ; :: thesis: ( ex n being Nat st not i2 . n = disjointify g,n or i1 = i2 )
assume A3: for n being Nat holds i2 . n = disjointify g,n ; :: thesis: i1 = i2

now

let n be Element of NAT ; :: thesis: i1 . n = i2 . n
i1 . n = disjointify g,n by A2;
hence i1 . n = i2 . n by A3; :: thesis: verum

end;

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