let D be non empty set ; :: thesis: for Q0, Q1 being FinSequence of D
for i being Element of NAT st 1 <= i & i <= len Q0 holds
(Q0 ^ Q1) /. i = Q0 /. i
let Q0, Q1 be FinSequence of D; :: thesis: for i being Element of NAT st 1 <= i & i <= len Q0 holds
(Q0 ^ Q1) /. i = Q0 /. i
let i be Element of NAT ; :: thesis: ( 1 <= i & i <= len Q0 implies (Q0 ^ Q1) /. i = Q0 /. i )
len Q0 <= (len Q0) + (len Q1) by NAT_1:11;
then A1: ( i <= len Q0 implies i <= (len Q0) + (len Q1) ) by XXREAL_0:2;
( i in dom Q0 implies i in Seg (len Q0) ) by FINSEQ_1:def 3;
then ( i in dom Q0 implies ( 1 <= i & i <= len (Q0 ^ Q1) ) ) by A1, FINSEQ_1:1, FINSEQ_1:22;
then A2: ( i in dom Q0 implies i in dom (Q0 ^ Q1) ) by FINSEQ_3:25;
( i in dom Q0 implies Q0 . i = Q0 /. i ) by PARTFUN1:def 6;
then A3: ( i in dom Q0 implies (Q0 ^ Q1) . i = Q0 /. i ) by FINSEQ_1:def 7;
( i in dom Q0 iff i in Seg (len Q0) ) by FINSEQ_1:def 3;
hence ( 1 <= i & i <= len Q0 implies (Q0 ^ Q1) /. i = Q0 /. i ) by A2, A3, FINSEQ_1:1, PARTFUN1:def 6; :: thesis: verum