let n1, n2 be Element of NAT ; for S being Gene-Set
for p1, p2 being Individual of S holds crossover (p1,p2,n1,n2) is Individual of S
let S be Gene-Set; for p1, p2 being Individual of S holds crossover (p1,p2,n1,n2) is Individual of S
let p1, p2 be Individual of S; crossover (p1,p2,n1,n2) is Individual of S
reconsider q1 = crossover (p1,p2,n1), q2 = crossover (p2,p1,n1) as Individual of S ;
crossover (q1,q2,n2) is Individual of S
;
hence
crossover (p1,p2,n1,n2) is Individual of S
; verum