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