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

proof

A2: len (crossover (p1,p2,n)) = (len (p1 | n)) + (len (p2 /^ n)) by FINSEQ_1:22;

now :: thesis: len (crossover (p1,p2,n)) = len S

per cases ( n <= len p1 or n > len p1 ) ;

suppose A3: n <= len p1 ; :: thesis: len (crossover (p1,p2,n)) = len S

len (p2 /^ n) = (len p2) -' n by RFINSEQ:29
.= (len S) -' n by Def1
.= (len p1) -' n by Def1
.= (len p1) - n by A3, XREAL_1:233 ;
then len (crossover (p1,p2,n)) = n + ((len p1) - n) by A2, A3, FINSEQ_1:59
.= len p1 ;
hence len (crossover (p1,p2,n)) = len S by Def1; :: thesis: verum

end;

suppose A4: n > len p1 ; :: thesis: len (crossover (p1,p2,n)) = len S

p1 | n = p1 | (Seg n) by FINSEQ_1:def 16;
then A5: p1 | n = p1 by A4, FINSEQ_2:20;
A6: (len p1) - n < 0 by A4, XREAL_1:49;
len (p2 /^ n) = (len p2) -' n by RFINSEQ:29
.= (len S) -' n by Def1
.= (len p1) -' n by Def1
.= 0 by A6, XREAL_0:def 2 ;
hence len (crossover (p1,p2,n)) = len S by A2, A5, Def1; :: thesis: verum

end;

end;

end;

hence len (crossover (p1,p2,n)) = len S ; :: thesis: verum

end;

for i being Element of NAT st i in dom (crossover (p1,p2,n)) holds
(crossover (p1,p2,n)) . i in S . i

proof

let i be Element of NAT ; :: thesis: ( i in dom (crossover (p1,p2,n)) implies (crossover (p1,p2,n)) . i in S . i )
assume A7: i in dom (crossover (p1,p2,n)) ; :: thesis: (crossover (p1,p2,n)) . i in S . i

now :: thesis: (crossover (p1,p2,n)) . i in S . i

per cases ( i in dom (p1 | n) or ex k being Nat st
( k in dom (p2 /^ n) & i = (len (p1 | n)) + k ) ) by A7, FINSEQ_1:25;

suppose A8: i in dom (p1 | n) ; :: thesis: (crossover (p1,p2,n)) . i in S . i

A9: dom (p1 | n) c= dom p1 by FINSEQ_5:18;
(p1 | n) . i = (p1 | n) /. i by A8, PARTFUN1:def 6
.= p1 /. i by A8, FINSEQ_4:70
.= p1 . i by A8, A9, PARTFUN1:def 6 ;
then (p1 | n) . i in S . i by A8, A9, Def1;
hence (crossover (p1,p2,n)) . i in S . i by A8, FINSEQ_1:def 7; :: thesis: verum

end;

suppose ex k being Nat st
( k in dom (p2 /^ n) & i = (len (p1 | n)) + k ) ; :: thesis: (crossover (p1,p2,n)) . i in S . i

then consider k being Nat such that
A10: k in dom (p2 /^ n) and
A11: i = (len (p1 | n)) + k ;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A12: n <= len (p1 | n)

proof

n + k in dom p2 by A10, FINSEQ_5:26;
then n + k in Seg (len p2) by FINSEQ_1:def 3;
then n + k <= len p2 by FINSEQ_1:1;
then n + k <= len S by Def1;
then n + k <= len p1 by Def1;
then A13: k <= (len p1) - n by XREAL_1:19;
k in Seg (len (p2 /^ n)) by A10, FINSEQ_1:def 3;
then 1 <= k by FINSEQ_1:1;
then 1 <= (len p1) - n by A13, XXREAL_0:2;
then 1 + n <= len p1 by XREAL_1:19;
then A14: n <= (len p1) - 1 by XREAL_1:19;
len p1 <= (len p1) + 1 by NAT_1:11;
then A15: (len p1) - 1 <= len p1 by XREAL_1:20;
assume n > len (p1 | n) ; :: thesis: contradiction
hence contradiction by A14, A15, FINSEQ_1:59, XXREAL_0:2; :: thesis: verum

end;

len (p1 | n) <= n by FINSEQ_5:17;
then A16: len (p1 | n) = n by A12, XXREAL_0:1;
then n + k in Seg (len S) by A1, A7, A11, FINSEQ_1:def 3;
then n + k in Seg (len p2) by Def1;
then A17: n + k in dom p2 by FINSEQ_1:def 3;
(crossover (p1,p2,n)) . i = (p2 /^ n) . k by A10, A11, FINSEQ_1:def 7
.= (p2 /^ n) /. k by A10, PARTFUN1:def 6
.= p2 /. (n + k) by A10, FINSEQ_5:27
.= p2 . (n + k) by A17, PARTFUN1:def 6 ;
hence (crossover (p1,p2,n)) . i in S . i by A11, A16, A17, Def1; :: thesis: verum

end;

end;

end;

hence (crossover (p1,p2,n)) . i in S . i ; :: thesis: verum

end;

hence crossover (p1,p2,n) is Individual of S by A1, Def1; :: thesis: verum