let n be Element of NAT ; 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; for p1, p2 being Individual of S holds crossover (p1,p2,n) is Individual of S
let p1, p2 be Individual of S; crossover (p1,p2,n) is Individual of S
A1:
len (crossover (p1,p2,n)) = len S
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 ;
( 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))
;
(crossover (p1,p2,n)) . i in S . i
now (crossover (p1,p2,n)) . i in S . iper 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
ex
k being
Nat st
(
k in dom (p2 /^ n) &
i = (len (p1 | n)) + k )
;
(crossover (p1,p2,n)) . i in S . ithen 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)
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;
verum end; end; end;
hence
(crossover (p1,p2,n)) . i in S . i
;
verum
end;
hence
crossover (p1,p2,n) is Individual of S
by A1, Def1; verum