let S be Gene-Set; :: thesis: for p1, p2 being Individual of S holds crossover (p1,p2,0,0,0,0,0) = p2
let p1, p2 be Individual of S; :: thesis: crossover (p1,p2,0,0,0,0,0) = p2
crossover (p1,p2,0,0,0,0,0) = crossover ((crossover (p1,p2,0,0,0,0)),p2,0) by Th32;
hence crossover (p1,p2,0,0,0,0,0) = p2 by Th4; :: thesis: verum