let p be Prime; :: thesis: for f1, f2 being FinSequence of NAT holds p |-count (f1 ^ f2) = (p |-count f1) ^ (p |-count f2)
let f1, f2 be FinSequence of NAT ; :: thesis: p |-count (f1 ^ f2) = (p |-count f1) ^ (p |-count f2)
A1: len (p |-count f2) = len f2 by Def1;
A2: dom (p |-count (f1 ^ f2)) = Seg (len (p |-count (f1 ^ f2))) by FINSEQ_1:def 3
.= Seg (len (f1 ^ f2)) by Def1 ;
A3: for k being Nat st k in dom (p |-count (f1 ^ f2)) holds
(p |-count (f1 ^ f2)) . k = ((p |-count f1) ^ (p |-count f2)) . k

proof

let k be Nat; :: thesis: ( k in dom (p |-count (f1 ^ f2)) implies (p |-count (f1 ^ f2)) . k = ((p |-count f1) ^ (p |-count f2)) . k )
assume A4: k in dom (p |-count (f1 ^ f2)) ; :: thesis: (p |-count (f1 ^ f2)) . k = ((p |-count f1) ^ (p |-count f2)) . k
then A5: k in dom (f1 ^ f2) by A2, FINSEQ_1:def 3;

per cases ( k in dom f1 or ex n being Nat st
( n in dom f2 & k = (len f1) + n ) ) by A5, FINSEQ_1:25;

suppose A6: k in dom f1 ; :: thesis: (p |-count (f1 ^ f2)) . k = ((p |-count f1) ^ (p |-count f2)) . k

A7: dom f1 = Seg (len f1) by FINSEQ_1:def 3
.= Seg (len (p |-count f1)) by Def1
.= dom (p |-count f1) by FINSEQ_1:def 3 ;
(p |-count (f1 ^ f2)) . k = p |-count ((f1 ^ f2) . k) by A4, Def1
.= p |-count (f1 . k) by A6, FINSEQ_1:def 7
.= (p |-count f1) . k by A6, A7, Def1 ;
hence (p |-count (f1 ^ f2)) . k = ((p |-count f1) ^ (p |-count f2)) . k by A6, A7, FINSEQ_1:def 7; :: thesis: verum

end;

suppose A8: ex n being Nat st
( n in dom f2 & k = (len f1) + n ) ; :: thesis: (p |-count (f1 ^ f2)) . k = ((p |-count f1) ^ (p |-count f2)) . k

A9: dom f2 = Seg (len f2) by FINSEQ_1:def 3
.= Seg (len (p |-count f2)) by Def1
.= dom (p |-count f2) by FINSEQ_1:def 3 ;
consider n being Nat such that
A10: n in dom f2 and
A11: k = (len f1) + n by A8;
A12: ((p |-count f1) ^ (p |-count f2)) . k = ((p |-count f1) ^ (p |-count f2)) . ((len (p |-count f1)) + n) by A11, Def1
.= (p |-count f2) . n by A10, A9, FINSEQ_1:def 7 ;
(f1 ^ f2) . k = f2 . n by A10, A11, FINSEQ_1:def 7;
then (p |-count (f1 ^ f2)) . k = p |-count (f2 . n) by A4, Def1
.= (p |-count f2) . n by A10, A9, Def1 ;
hence (p |-count (f1 ^ f2)) . k = ((p |-count f1) ^ (p |-count f2)) . k by A12; :: thesis: verum

end;

end;

end;

Seg (len (f1 ^ f2)) = Seg ((len f1) + (len f2)) by FINSEQ_1:22
.= Seg ((len (p |-count f1)) + (len (p |-count f2))) by A1, Def1
.= Seg (len ((p |-count f1) ^ (p |-count f2))) by FINSEQ_1:22
.= dom ((p |-count f1) ^ (p |-count f2)) by FINSEQ_1:def 3 ;
hence p |-count (f1 ^ f2) = (p |-count f1) ^ (p |-count f2) by A2, A3, FINSEQ_1:13; :: thesis: verum