let G be Group; :: thesis: for f, g being FinSequence of G holds (f ^ g) " = (f ") ^ (g ")
let f, g be FinSequence of G; :: thesis: (f ^ g) " = (f ") ^ (g ")
A1: len ((f ^ g) ") = len (f ^ g) by Def3
.= (len f) + (len g) by FINSEQ_1:22 ;
A2: (len f) + (len g) = (len (f ")) + (len g) by Def3
.= (len (f ")) + (len (g ")) by Def3
.= len ((f ") ^ (g ")) by FINSEQ_1:22 ;
A3: len ((f ^ g) ") = len (f ^ g) by Def3;
for i being Nat st 1 <= i & i <= len ((f ^ g) ") holds
((f ^ g) ") . i = ((f ") ^ (g ")) . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len ((f ^ g) ") implies ((f ^ g) ") . i = ((f ") ^ (g ")) . i )
assume that
A4: 1 <= i and
A5: i <= len ((f ^ g) ") ; :: thesis: ((f ^ g) ") . i = ((f ") ^ (g ")) . i

now :: thesis: ( ( len f > 0 & ((f ^ g) ") . i = ((f ") ^ (g ")) . i ) or ( len f <= 0 & ((f ^ g) ") . i = ((f ") ^ (g ")) . i ) )

per cases ( len f > 0 or len f <= 0 ) ;

case len f > 0 ; :: thesis: ((f ^ g) ") . i = ((f ") ^ (g ")) . i

A6: len (f ") = len f by Def3;
len ((f ^ g) ") = len (f ^ g) by Def3;
then A7: dom ((f ^ g) ") = dom (f ^ g) by FINSEQ_3:29;
i in Seg (len ((f ^ g) ")) by A4, A5;
then A8: i in dom ((f ^ g) ") by FINSEQ_1:def 3;
then A9: ((f ^ g) ") . i = ((f ^ g) ") /. i by PARTFUN1:def 6
.= ((f ^ g) /. i) " by A7, A8, Def3 ;
A10: len (g ") = len g by Def3;

now :: thesis: ( ( i <= len f & ((f ^ g) ") . i = ((f ") ^ (g ")) . i ) or ( i > len f & ((f ^ g) ") . i = ((f ") ^ (g ")) . i ) )

per cases ( i <= len f or i > len f ) ;

case i <= len f ; :: thesis: ((f ^ g) ") . i = ((f ") ^ (g ")) . i

then A11: i in Seg (len f) by A4;
then A12: i in dom f by FINSEQ_1:def 3;
A13: i in dom (f ") by A6, A11, FINSEQ_1:def 3;
(f ^ g) /. i = (f ^ g) . i by A7, A8, PARTFUN1:def 6
.= f . i by A12, FINSEQ_1:def 7
.= f /. i by A12, PARTFUN1:def 6 ;
then ((f ^ g) /. i) " = (f ") /. i by A12, Def3
.= (f ") . i by A13, PARTFUN1:def 6 ;
hence ((f ^ g) ") . i = ((f ") ^ (g ")) . i by A9, A13, FINSEQ_1:def 7; :: thesis: verum

end;

case A14: i > len f ; :: thesis: ((f ^ g) ") . i = ((f ") ^ (g ")) . i

then 1 + (len f) <= i by NAT_1:13;
then A15: (1 + (len f)) - (len f) <= i - (len f) by XREAL_1:9;
A16: i -' (len f) = i - (len f) by A14, XREAL_1:233;
i - (len f) <= ((len g) + (len f)) - (len f) by A1, A5, XREAL_1:9;
then A17: i -' (len f) in Seg (len g) by A16, A15;
then A18: i -' (len f) in dom g by FINSEQ_1:def 3;
A19: i -' (len f) in dom (g ") by A10, A17, FINSEQ_1:def 3;
(f ^ g) /. i = (f ^ g) . i by A7, A8, PARTFUN1:def 6
.= g . (i - (len f)) by A3, A5, A14, FINSEQ_1:24
.= g /. (i -' (len f)) by A16, A18, PARTFUN1:def 6 ;
then ((f ^ g) /. i) " = (g ") /. (i -' (len f)) by A18, Def3
.= (g ") . (i - (len (f "))) by A6, A16, A19, PARTFUN1:def 6 ;
hence ((f ^ g) ") . i = ((f ") ^ (g ")) . i by A1, A2, A5, A6, A9, A14, FINSEQ_1:24; :: thesis: verum

end;

end;

end;

hence ((f ^ g) ") . i = ((f ") ^ (g ")) . i ; :: thesis: verum

end;

case len f <= 0 ; :: thesis: ((f ^ g) ") . i = ((f ") ^ (g ")) . i

then f = {} ;
then ( (f ^ g) " = g " & f " = <*> the carrier of G ) by Th20, FINSEQ_1:34;
hence ((f ^ g) ") . i = ((f ") ^ (g ")) . i by FINSEQ_1:34; :: thesis: verum

end;

end;

end;

hence ((f ^ g) ") . i = ((f ") ^ (g ")) . i ; :: thesis: verum

end;

hence (f ^ g) " = (f ") ^ (g ") by A1, A2; :: thesis: verum