let n1, n2, n3, n4, n5 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,n5 = crossover p1,p2,n2,n3,n4,n5 ) & ( n2 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n3,n4,n5 ) & ( n3 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n2,n4,n5 ) & ( n4 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n2,n3,n5 ) & ( n5 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n2,n3,n4 ) )
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,n5 = crossover p1,p2,n2,n3,n4,n5 ) & ( n2 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n3,n4,n5 ) & ( n3 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n2,n4,n5 ) & ( n4 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n2,n3,n5 ) & ( n5 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n2,n3,n4 ) )
let p1, p2 be Individual of S; :: thesis: ( ( n1 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n2,n3,n4,n5 ) & ( n2 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n3,n4,n5 ) & ( n3 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n2,n4,n5 ) & ( n4 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n2,n3,n5 ) & ( n5 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n2,n3,n4 ) )
A1: ( n5 >= len p1 implies crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n1,n2,n3,n4 )

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

assume A12: n1 >= len p1 ; :: thesis: crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n2,n3,n4,n5
then n1 >= len S by Def1;
then A13: n1 >= len p2 by Def1;
crossover p1,p2,n1,n2,n3,n4,n5 = crossover (crossover p1,p2,n2,n3,n4),(crossover p2,p1,n1,n2,n3,n4),n5 by A12, Th33
.= crossover (crossover p1,p2,n2,n3,n4),(crossover p2,p1,n2,n3,n4),n5 by A13, Th33 ;
hence crossover p1,p2,n1,n2,n3,n4,n5 = crossover p1,p2,n2,n3,n4,n5 ; :: thesis: verum

end;

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