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

let S be Gene-Set; :: thesis: for p1, p2 being Individual of S holds crossover (p1,p2,n1,n1) = p1
let p1, p2 be Individual of S; :: thesis: crossover (p1,p2,n1,n1) = p1
A1: ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1
proof
now :: thesis: ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1
per cases ( n1 <= len p2 or n1 > len p2 ) ;
suppose n1 <= len p2 ; :: thesis: ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1
then len (p2 | n1) = n1 by FINSEQ_1:59;
hence ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1 by FINSEQ_5:37; :: thesis: verum
end;
suppose n1 > len p2 ; :: thesis: ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1
then A2: n1 > len S by Def1;
then n1 > len (crossover (p2,p1,n1)) by Def1;
then A3: ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = {} by FINSEQ_5:32;
n1 > len p1 by ;
hence ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1 by ; :: thesis: verum
end;
end;
end;
hence ((p2 | n1) ^ (p1 /^ n1)) /^ n1 = p1 /^ n1 ; :: thesis: verum
end;
((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1
proof
now :: thesis: ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1
per cases ( n1 <= len p1 or n1 > len p1 ) ;
suppose n1 <= len p1 ; :: thesis: ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1
then len (p1 | n1) = n1 by FINSEQ_1:59;
hence ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1 by FINSEQ_5:23; :: thesis: verum
end;
suppose A4: n1 > len p1 ; :: thesis: ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1
then A5: n1 > len S by Def1;
then A6: n1 > len p2 by Def1;
n1 > len (crossover (p1,p2,n1)) by ;
then ((p1 | n1) ^ (p2 /^ n1)) | n1 = (p1 | n1) ^ (p2 /^ n1) by FINSEQ_1:58
.= p1 ^ (p2 /^ n1) by
.= p1 ^ {} by
.= p1 by FINSEQ_1:34
.= p1 | n1 by ;
hence ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1 ; :: thesis: verum
end;
end;
end;
hence ((p1 | n1) ^ (p2 /^ n1)) | n1 = p1 | n1 ; :: thesis: verum
end;
hence crossover (p1,p2,n1,n1) = p1 by ; :: thesis: verum