let n1, n2, n3, n4 be Element of NAT ; for S being Gene-Set
for p1, p2 being Individual of S holds
( crossover p1,p2,n1,0 ,0 ,0 = crossover p2,p1,n1 & crossover p1,p2,0 ,n2,0 ,0 = crossover p2,p1,n2 & crossover p1,p2,0 ,0 ,n3,0 = crossover p2,p1,n3 & crossover p1,p2,0 ,0 ,0 ,n4 = crossover p2,p1,n4 )
let S be Gene-Set; for p1, p2 being Individual of S holds
( crossover p1,p2,n1,0 ,0 ,0 = crossover p2,p1,n1 & crossover p1,p2,0 ,n2,0 ,0 = crossover p2,p1,n2 & crossover p1,p2,0 ,0 ,n3,0 = crossover p2,p1,n3 & crossover p1,p2,0 ,0 ,0 ,n4 = crossover p2,p1,n4 )
let p1, p2 be Individual of S; ( crossover p1,p2,n1,0 ,0 ,0 = crossover p2,p1,n1 & crossover p1,p2,0 ,n2,0 ,0 = crossover p2,p1,n2 & crossover p1,p2,0 ,0 ,n3,0 = crossover p2,p1,n3 & crossover p1,p2,0 ,0 ,0 ,n4 = crossover p2,p1,n4 )
crossover p1,p2,n1,0 ,0 ,0 = crossover p1,p2,n1,0
by Th30;
hence
crossover p1,p2,n1,0 ,0 ,0 = crossover p2,p1,n1
by Th8; ( crossover p1,p2,0 ,n2,0 ,0 = crossover p2,p1,n2 & crossover p1,p2,0 ,0 ,n3,0 = crossover p2,p1,n3 & crossover p1,p2,0 ,0 ,0 ,n4 = crossover p2,p1,n4 )
crossover p1,p2,0 ,n2,0 ,0 = crossover p1,p2,0 ,n2
by Th30;
hence
crossover p1,p2,0 ,n2,0 ,0 = crossover p2,p1,n2
by Th7; ( crossover p1,p2,0 ,0 ,n3,0 = crossover p2,p1,n3 & crossover p1,p2,0 ,0 ,0 ,n4 = crossover p2,p1,n4 )
crossover p1,p2,0 ,0 ,n3,0 = crossover p1,p2,0 ,n3
by Th30;
hence
crossover p1,p2,0 ,0 ,n3,0 = crossover p2,p1,n3
by Th7; crossover p1,p2,0 ,0 ,0 ,n4 = crossover p2,p1,n4
crossover p1,p2,0 ,0 ,0 ,n4 = crossover p1,p2,0 ,n4
by Th30;
hence
crossover p1,p2,0 ,0 ,0 ,n4 = crossover p2,p1,n4
by Th7; verum