let n1, n2, n3, n4 be Element of NAT ; :: thesis: for S being Gene-Set
for p1, p2 being Individual of S holds
( crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n4,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n2,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n4,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n4,n3,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n1,n3,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n1,n4,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n1,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n4,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4,n1,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4,n3,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n2,n1,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n2,n4,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4,n1,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4,n2,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n2,n3,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n3,n2,n1 )

let S be Gene-Set; :: thesis: for p1, p2 being Individual of S holds
( crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n4,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n2,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n4,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n4,n3,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n1,n3,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n1,n4,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n1,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n4,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4,n1,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4,n3,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n2,n1,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n2,n4,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4,n1,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4,n2,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n2,n3,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n3,n2,n1 )

let p1, p2 be Individual of S; :: thesis: ( crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n4,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n2,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n4,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n4,n3,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n1,n3,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n1,n4,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n1,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n4,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4,n1,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4,n3,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n2,n1,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n2,n4,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4,n1,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4,n2,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n2,n3,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n3,n2,n1 )
A1: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n4,n3
proof
set q2 = crossover p2,p1,n1,n2;
set q1 = crossover p1,p2,n1,n2;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n1,n2),(crossover p2,p1,n1,n2),n3,n4
.= crossover (crossover p1,p2,n1,n2),(crossover p2,p1,n1,n2),n4,n3 by Th13
.= crossover (crossover (crossover p1,p2,n1,n2),(crossover p2,p1,n1,n2),n4),(crossover (crossover p2,p1,n1,n2),(crossover p1,p2,n1,n2),n4),n3 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n4,n3 ; :: thesis: verum
end;
A2: crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n1,n3,n2),(crossover p2,p1,n1,n2,n3),n4 by Th25
.= crossover (crossover p1,p2,n1,n3,n2),(crossover p2,p1,n1,n3,n2),n4 by Th25 ;
A3: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n4,n1
proof
set q2 = crossover p2,p1,n2,n3;
set q1 = crossover p1,p2,n2,n3;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n2,n1,n3),(crossover p2,p1,n1,n2,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n3,n1),(crossover p2,p1,n1,n2,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n3,n1),(crossover p2,p1,n2,n1,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n3,n1),(crossover p2,p1,n2,n3,n1),n4 by Th25
.= crossover (crossover p1,p2,n2,n3),(crossover p2,p1,n2,n3),n1,n4
.= crossover (crossover p1,p2,n2,n3),(crossover p2,p1,n2,n3),n4,n1 by Th13
.= crossover (crossover p1,p2,n2,n3,n4),(crossover p2,p1,n2,n3,n4),n1 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n4,n1 ; :: thesis: verum
end;
A4: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n4,n3,n2
proof
set q2 = crossover p2,p1,n1,n3;
set q1 = crossover p1,p2,n1,n3;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n1,n3,n2),(crossover p2,p1,n1,n2,n3),n4 by Th25
.= crossover (crossover p1,p2,n1,n3,n2),(crossover p2,p1,n1,n3,n2),n4 by Th25
.= crossover (crossover p1,p2,n1,n3),(crossover p2,p1,n1,n3),n2,n4
.= crossover (crossover p1,p2,n1,n3),(crossover p2,p1,n1,n3),n4,n2 by Th13
.= crossover (crossover p1,p2,n1,n3,n4),(crossover p2,p1,n1,n3,n4),n2
.= crossover (crossover p1,p2,n1,n4,n3),(crossover p2,p1,n1,n3,n4),n2 by Th25
.= crossover (crossover p1,p2,n1,n4,n3),(crossover p2,p1,n1,n4,n3),n2 by Th25 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n4,n3,n2 ; :: thesis: verum
end;
A5: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n3,n2,n1
proof
set q2 = crossover p2,p1,n3,n2;
set q1 = crossover p1,p2,n3,n2;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n3,n1,n2),(crossover p2,p1,n1,n2,n3),n4 by Th26
.= crossover (crossover p1,p2,n3,n1,n2),(crossover p2,p1,n3,n1,n2),n4 by Th26
.= crossover (crossover p1,p2,n3,n2,n1),(crossover p2,p1,n3,n1,n2),n4 by Th25
.= crossover (crossover p1,p2,n3,n2,n1),(crossover p2,p1,n3,n2,n1),n4 by Th25
.= crossover (crossover p1,p2,n3,n2),(crossover p2,p1,n3,n2),n1,n4
.= crossover (crossover p1,p2,n3,n2),(crossover p2,p1,n3,n2),n4,n1 by Th13
.= crossover (crossover p1,p2,n3,n2,n4),(crossover p2,p1,n3,n2,n4),n1
.= crossover (crossover p1,p2,n4,n3,n2),(crossover p2,p1,n3,n2,n4),n1 by Th26
.= crossover (crossover p1,p2,n4,n3,n2),(crossover p2,p1,n4,n3,n2),n1 by Th26 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n3,n2,n1 ; :: thesis: verum
end;
A6: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n1,n4,n3
proof
set q2 = crossover p2,p1,n2,n1;
set q1 = crossover p1,p2,n2,n1;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n2,n1,n3),(crossover p2,p1,n1,n2,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n1,n3),(crossover p2,p1,n2,n1,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n1),(crossover p2,p1,n2,n1),n3,n4
.= crossover (crossover p1,p2,n2,n1),(crossover p2,p1,n2,n1),n4,n3 by Th13
.= crossover (crossover p1,p2,n2,n1,n4),(crossover p2,p1,n2,n1,n4),n3 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n1,n4,n3 ; :: thesis: verum
end;
A7: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n2,n3,n1
proof
set q2 = crossover p2,p1,n2,n3;
set q1 = crossover p1,p2,n2,n3;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n2,n1,n3),(crossover p2,p1,n1,n2,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n1,n3),(crossover p2,p1,n2,n1,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n3,n1),(crossover p2,p1,n2,n1,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n3,n1),(crossover p2,p1,n2,n3,n1),n4 by Th25
.= crossover (crossover p1,p2,n2,n3),(crossover p2,p1,n2,n3),n1,n4
.= crossover (crossover p1,p2,n2,n3),(crossover p2,p1,n2,n3),n4,n1 by Th13
.= crossover (crossover p1,p2,n2,n3,n4),(crossover p2,p1,n2,n3,n4),n1
.= crossover (crossover p1,p2,n4,n2,n3),(crossover p2,p1,n2,n3,n4),n1 by Th26
.= crossover (crossover p1,p2,n4,n2,n3),(crossover p2,p1,n4,n2,n3),n1 by Th26 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n2,n3,n1 ; :: thesis: verum
end;
A8: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n4,n2
proof
set q2 = crossover p2,p1,n1,n3;
set q1 = crossover p1,p2,n1,n3;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n1,n3,n2),(crossover p2,p1,n1,n2,n3),n4 by Th25
.= crossover (crossover p1,p2,n1,n3,n2),(crossover p2,p1,n1,n3,n2),n4 by Th25
.= crossover (crossover p1,p2,n1,n3),(crossover p2,p1,n1,n3),n2,n4
.= crossover (crossover p1,p2,n1,n3),(crossover p2,p1,n1,n3),n4,n2 by Th13
.= crossover (crossover (crossover p1,p2,n1,n3),(crossover p2,p1,n1,n3),n4),(crossover (crossover p2,p1,n1,n3),(crossover p1,p2,n1,n3),n4),n2 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n4,n2 ; :: thesis: verum
end;
A9: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n2,n4,n1
proof
set q2 = crossover p2,p1,n3,n2;
set q1 = crossover p1,p2,n3,n2;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n3,n1,n2),(crossover p2,p1,n1,n2,n3),n4 by Th26
.= crossover (crossover p1,p2,n3,n1,n2),(crossover p2,p1,n3,n1,n2),n4 by Th26
.= crossover (crossover p1,p2,n3,n2,n1),(crossover p2,p1,n3,n1,n2),n4 by Th25
.= crossover (crossover p1,p2,n3,n2,n1),(crossover p2,p1,n3,n2,n1),n4 by Th25
.= crossover (crossover p1,p2,n3,n2),(crossover p2,p1,n3,n2),n1,n4
.= crossover (crossover p1,p2,n3,n2),(crossover p2,p1,n3,n2),n4,n1 by Th13
.= crossover (crossover p1,p2,n3,n2,n4),(crossover p2,p1,n3,n2,n4),n1 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n2,n4,n1 ; :: thesis: verum
end;
A10: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4,n1,n3
proof
set q2 = crossover p2,p1,n2,n1;
set q1 = crossover p1,p2,n2,n1;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n2,n1,n3),(crossover p2,p1,n1,n2,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n1,n3),(crossover p2,p1,n2,n1,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n1),(crossover p2,p1,n2,n1),n3,n4
.= crossover (crossover p1,p2,n2,n1),(crossover p2,p1,n2,n1),n4,n3 by Th13
.= crossover (crossover p1,p2,n2,n1,n4),(crossover p2,p1,n2,n1,n4),n3
.= crossover (crossover p1,p2,n2,n4,n1),(crossover p2,p1,n2,n1,n4),n3 by Th25
.= crossover (crossover p1,p2,n2,n4,n1),(crossover p2,p1,n2,n4,n1),n3 by Th25 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4,n1,n3 ; :: thesis: verum
end;
A11: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4,n2,n1
proof
set q2 = crossover p2,p1,n3,n2;
set q1 = crossover p1,p2,n3,n2;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n3,n1,n2),(crossover p2,p1,n1,n2,n3),n4 by Th26
.= crossover (crossover p1,p2,n3,n1,n2),(crossover p2,p1,n3,n1,n2),n4 by Th26
.= crossover (crossover p1,p2,n3,n2,n1),(crossover p2,p1,n3,n1,n2),n4 by Th25
.= crossover (crossover p1,p2,n3,n2,n1),(crossover p2,p1,n3,n2,n1),n4 by Th25
.= crossover (crossover p1,p2,n3,n2),(crossover p2,p1,n3,n2),n1,n4
.= crossover (crossover p1,p2,n3,n2),(crossover p2,p1,n3,n2),n4,n1 by Th13
.= crossover (crossover p1,p2,n3,n2,n4),(crossover p2,p1,n3,n2,n4),n1
.= crossover (crossover p1,p2,n3,n4,n2),(crossover p2,p1,n3,n2,n4),n1 by Th25
.= crossover (crossover p1,p2,n3,n4,n2),(crossover p2,p1,n3,n4,n2),n1 by Th25 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4,n2,n1 ; :: thesis: verum
end;
A12: crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n3,n1,n2),(crossover p2,p1,n1,n2,n3),n4 by Th26
.= crossover (crossover p1,p2,n3,n1,n2),(crossover p2,p1,n3,n1,n2),n4 by Th26
.= crossover (crossover p1,p2,n3,n2,n1),(crossover p2,p1,n3,n1,n2),n4 by Th25
.= crossover (crossover p1,p2,n3,n2,n1),(crossover p2,p1,n3,n2,n1),n4 by Th25 ;
A13: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4,n1,n2
proof
set q2 = crossover p2,p1,n3,n1;
set q1 = crossover p1,p2,n3,n1;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n3,n1,n2),(crossover p2,p1,n1,n2,n3),n4 by Th26
.= crossover (crossover p1,p2,n3,n1,n2),(crossover p2,p1,n3,n1,n2),n4 by Th26
.= crossover (crossover p1,p2,n3,n1),(crossover p2,p1,n3,n1),n2,n4
.= crossover (crossover p1,p2,n3,n1),(crossover p2,p1,n3,n1),n4,n2 by Th13
.= crossover (crossover p1,p2,n3,n1,n4),(crossover p2,p1,n3,n1,n4),n2
.= crossover (crossover p1,p2,n3,n4,n1),(crossover p2,p1,n3,n1,n4),n2 by Th25
.= crossover (crossover p1,p2,n3,n4,n1),(crossover p2,p1,n3,n4,n1),n2 by Th25 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4,n1,n2 ; :: thesis: verum
end;
A14: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4,n3,n1
proof
set q2 = crossover p2,p1,n2,n3;
set q1 = crossover p1,p2,n2,n3;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n2,n1,n3),(crossover p2,p1,n1,n2,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n3,n1),(crossover p2,p1,n1,n2,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n3,n1),(crossover p2,p1,n2,n1,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n3,n1),(crossover p2,p1,n2,n3,n1),n4 by Th25
.= crossover (crossover p1,p2,n2,n3),(crossover p2,p1,n2,n3),n1,n4
.= crossover (crossover p1,p2,n2,n3),(crossover p2,p1,n2,n3),n4,n1 by Th13
.= crossover (crossover p1,p2,n2,n3,n4),(crossover p2,p1,n2,n3,n4),n1
.= crossover (crossover p1,p2,n2,n4,n3),(crossover p2,p1,n2,n3,n4),n1 by Th25
.= crossover (crossover p1,p2,n2,n4,n3),(crossover p2,p1,n2,n4,n3),n1 by Th25 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4,n3,n1 ; :: thesis: verum
end;
A15: crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n2,n1,n3),(crossover p2,p1,n1,n2,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n1,n3),(crossover p2,p1,n2,n1,n3),n4 by Th25 ;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n2,n1,n3),(crossover p2,p1,n1,n2,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n1,n3),(crossover p2,p1,n2,n1,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n3,n1),(crossover p2,p1,n2,n1,n3),n4 by Th25
.= crossover (crossover p1,p2,n2,n3,n1),(crossover p2,p1,n2,n3,n1),n4 by Th25 ;
hence ( crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n4,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n2,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n4,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n4,n3,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n1,n3,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n1,n4,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n1,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n4,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4,n1,n3 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n4,n3,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n2,n1,n4 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n2,n4,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4,n1,n2 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n3,n4,n2,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n2,n3,n1 & crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n4,n3,n2,n1 ) by A2, A15, A1, A8, A4, A6, A3, A10, A14, A12, A9, A13, A11, A7, A5; :: thesis: verum