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

proof

assume n4 >= len p1 ; :: thesis: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n3
then n4 >= len S by Def1;
then A2: n4 >= len (crossover p1,p2,n1,n2,n3) by Def1;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n1,n2,n3),(crossover p2,p1,n1,n2,n3),n4 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n3 by A2, Th5; :: thesis: verum

end;

A3: ( n2 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n4 )

proof

assume A4: n2 >= len p1 ; :: thesis: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n4
then n2 >= len S by Def1;
then A5: n2 >= len p2 by Def1;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n1,n3),(crossover p2,p1,n1,n2,n3),n4 by A4, Th19
.= crossover (crossover p1,p2,n1,n3),(crossover p2,p1,n1,n3),n4 by A5, Th19 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n4 ; :: thesis: verum

end;

A6: ( n3 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n4 )

proof

assume A7: n3 >= len p1 ; :: thesis: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n4
then n3 >= len S by Def1;
then A8: n3 >= len p2 by Def1;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n1,n2),(crossover p2,p1,n1,n2,n3),n4 by A7, Th20
.= crossover (crossover p1,p2,n1,n2),(crossover p2,p1,n1,n2),n4 by A8, Th20 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n4 ; :: thesis: verum

end;

( n1 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n4 )

proof

assume A9: n1 >= len p1 ; :: thesis: crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n4
then n1 >= len S by Def1;
then A10: n1 >= len p2 by Def1;
crossover p1,p2,n1,n2,n3,n4 = crossover (crossover p1,p2,n2,n3),(crossover p2,p1,n1,n2,n3),n4 by A9, Th18
.= crossover (crossover p1,p2,n2,n3),(crossover p2,p1,n2,n3),n4 by A10, Th18 ;
hence crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n4 ; :: thesis: verum

end;

hence ( ( n1 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n2,n3,n4 ) & ( n2 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n3,n4 ) & ( n3 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n4 ) & ( n4 >= len p1 implies crossover p1,p2,n1,n2,n3,n4 = crossover p1,p2,n1,n2,n3 ) ) by A3, A6, A1; :: thesis: verum