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 Def4;
A2: len ((f ^ g) " ) = len (f ^ g) by Def4
.= (len f) + (len g) by FINSEQ_1:35 ;
A3: (len f) + (len g) = (len (f " )) + (len g) by Def4
.= (len (f " )) + (len (g " )) by Def4
.= len ((f " ) ^ (g " )) by FINSEQ_1:35 ;
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 A4: ( 1 <= i & i <= len ((f ^ g) " ) ) ; :: thesis: ((f ^ g) " ) . i = ((f " ) ^ (g " )) . i
A5: i in NAT by ORDINAL1:def 13;

now

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 Def4;
A7: len (g " ) = len g by Def4;
len ((f ^ g) " ) = len (f ^ g) by Def4;
then A8: dom ((f ^ g) " ) = dom (f ^ g) by FINSEQ_3:31;
i in Seg (len ((f ^ g) " )) by A4, A5;
then A9: i in dom ((f ^ g) " ) by FINSEQ_1:def 3;
then A10: ((f ^ g) " ) . i = ((f ^ g) " ) /. i by PARTFUN1:def 8
.= ((f ^ g) /. i) " by A8, A9, Def4 ;

now

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, A5;
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 A8, A9, PARTFUN1:def 8
.= f . i by A12, FINSEQ_1:def 7
.= f /. i by A12, PARTFUN1:def 8 ;
then ((f ^ g) /. i) " = (f " ) /. i by A12, Def4
.= (f " ) . i by A13, PARTFUN1:def 8 ;
hence ((f ^ g) " ) . i = ((f " ) ^ (g " )) . i by A10, A13, FINSEQ_1:def 7; :: thesis: verum

end;

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

then A15: i -' (len f) = i - (len f) by XREAL_1:235;
1 + (len f) <= i by A14, NAT_1:13;
then A16: (1 + (len f)) - (len f) <= i - (len f) by XREAL_1:11;
i - (len f) <= ((len g) + (len f)) - (len f) by A2, A4, XREAL_1:11;
then A17: i -' (len f) in Seg (len g) by A15, A16;
then A18: i -' (len f) in dom g by FINSEQ_1:def 3;
A19: i -' (len f) in dom (g " ) by A7, A17, FINSEQ_1:def 3;
(f ^ g) /. i = (f ^ g) . i by A8, A9, PARTFUN1:def 8
.= g . (i - (len f)) by A1, A4, A14, FINSEQ_1:37
.= g /. (i -' (len f)) by A15, A18, PARTFUN1:def 8 ;
then ((f ^ g) /. i) " = (g " ) /. (i -' (len f)) by A18, Def4
.= (g " ) . (i - (len (f " ))) by A6, A15, A19, PARTFUN1:def 8 ;
hence ((f ^ g) " ) . i = ((f " ) ^ (g " )) . i by A2, A3, A4, A6, A10, A14, FINSEQ_1:37; :: 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 len f = 0 ;
then A20: f = {} ;
then A21: (f ^ g) " = g " by FINSEQ_1:47;
f " = <*> the carrier of G by A20, Th21;
hence ((f ^ g) " ) . i = ((f " ) ^ (g " )) . i by A21, FINSEQ_1:47; :: thesis: verum

end;

end;

end;

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

end;

hence (f ^ g) " = (f " ) ^ (g " ) by A2, A3, FINSEQ_1:18; :: thesis: verum