let I, X be non empty set ; :: thesis: for x being X -valued ManySortedSet of I
for p, q being FinSequence of I holds (p ^ q) * x = (p * x) ^ (q * x)
let x be X -valued ManySortedSet of I; :: thesis: for p, q being FinSequence of I holds (p ^ q) * x = (p * x) ^ (q * x)
let p, q be FinSequence of I; :: thesis: (p ^ q) * x = (p * x) ^ (q * x)
A1: dom x = I by PARTFUN1:def 2;
rng x c= X by RELAT_1:def 19;
then A2: x is Function of I,X by A1, FUNCT_2:2;
then A3: ( dom (p * x) = dom p & dom (q * x) = dom q & dom ((p ^ q) * x) = dom (p ^ q) ) by FINSEQ_3:120;
A4: dom (p ^ q) = Seg ((len p) + (len q)) by FINSEQ_1:def 7;
A5: ( Seg (len (p * x)) = dom p & Seg (len (q * x)) = dom q ) by A3, FINSEQ_1:def 3;
A6: ( len (p * x) = len p & len (q * x) = len q ) by A5, FINSEQ_1:def 3;
then A7: dom ((p * x) ^ (q * x)) = Seg ((len p) + (len q)) by FINSEQ_1:def 7;
for t being object st t in dom ((p ^ q) * x) holds
((p ^ q) * x) . t = ((p * x) ^ (q * x)) . t

proof

let t be object ; :: thesis: ( t in dom ((p ^ q) * x) implies ((p ^ q) * x) . t = ((p * x) ^ (q * x)) . t )
assume A8: t in dom ((p ^ q) * x) ; :: thesis: ((p ^ q) * x) . t = ((p * x) ^ (q * x)) . t
A9: t in dom (p ^ q) by A2, FINSEQ_3:120, A8;
A10: ((p ^ q) * x) . t = x . ((p ^ q) . t) by A2, FINSEQ_3:120, A8;

now :: thesis: ( ( t in dom p implies ((p ^ q) * x) . t = ((p * x) ^ (q * x)) . t ) & ( ex n being Nat st
( n in dom q & t = (len p) + n ) implies ((p ^ q) * x) . t = ((p * x) ^ (q * x)) . t ) )

hereby :: thesis: ( ex n being Nat st
( n in dom q & t = (len p) + n ) implies ((p ^ q) * x) . t = ((p * x) ^ (q * x)) . t )

assume A11: t in dom p ; :: thesis: ((p ^ q) * x) . t = ((p * x) ^ (q * x)) . t
then A12: ( x . ((p ^ q) . t) = x . (p . t) & x . (p . t) = (p * x) . t ) by FINSEQ_1:def 7, FUNCT_1:13;
t in dom (p * x) by A11, A2, FINSEQ_3:120;
hence ((p ^ q) * x) . t = ((p * x) ^ (q * x)) . t by A12, A10, FINSEQ_1:def 7; :: thesis: verum

end;

assume ex n being Nat st
( n in dom q & t = (len p) + n ) ; :: thesis: ((p ^ q) * x) . t = ((p * x) ^ (q * x)) . t
then consider n being Nat such that
A13: n in dom q and
A14: t = (len p) + n ;
A15: x . ((p ^ q) . ((len p) + n)) = x . (q . n) by A13, FINSEQ_1:def 7;
n in dom (q * x) by A13, A2, FINSEQ_3:120;
then ((p * x) ^ (q * x)) . ((len p) + n) = (q * x) . n by A6, FINSEQ_1:def 7;
hence ((p ^ q) * x) . t = ((p * x) ^ (q * x)) . t by A13, A14, A15, A10, FUNCT_1:13; :: thesis: verum

end;

hence ((p ^ q) * x) . t = ((p * x) ^ (q * x)) . t by A9, FINSEQ_1:25; :: thesis: verum

end;

hence (p ^ q) * x = (p * x) ^ (q * x) by A7, A2, FINSEQ_3:120, A4; :: thesis: verum