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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

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

end;

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

proof

assume A15: n1 >= len p1 ; :: thesis: crossover p1,p2,n1,n2,n3,n4,n5,n6 = crossover p1,p2,n2,n3,n4,n5,n6
then n1 >= len S by Def1;
then A16: n1 >= len p2 by Def1;
crossover p1,p2,n1,n2,n3,n4,n5,n6 = crossover (crossover p1,p2,n2,n3,n4,n5),(crossover p2,p1,n1,n2,n3,n4,n5),n6 by A15, Th46
.= crossover (crossover p1,p2,n2,n3,n4,n5),(crossover p2,p1,n2,n3,n4,n5),n6 by A16, Th46 ;
hence crossover p1,p2,n1,n2,n3,n4,n5,n6 = crossover p1,p2,n2,n3,n4,n5,n6 ; :: thesis: verum

end;

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