let S be Gene-Set; :: thesis: for p1, p2 being Individual of S holds crossover (p1,p2,0) = p2
let p1, p2 be Individual of S; :: thesis: crossover (p1,p2,0) = p2
crossover (p1,p2,0) = p2 /^ 0 by FINSEQ_1:34
.= p2 by FINSEQ_5:28 ;
hence crossover (p1,p2,0) = p2 ; :: thesis: verum