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 :: thesis: for n being Element of NAT holds i1 . n = i2 . n

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:63; :: thesis: verum