let L be non empty multMagma ; :: thesis: for p, q, r being sequence of L
for t being FinSequence of 3 -tuples_on NAT
for P being Permutation of (dom t)
for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
let p, q, r be sequence of L; :: thesis: for t being FinSequence of 3 -tuples_on NAT
for P being Permutation of (dom t)
for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
let t be FinSequence of 3 -tuples_on NAT; :: thesis: for P being Permutation of (dom t)
for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
let P be Permutation of (dom t); :: thesis: for t1 being FinSequence of 3 -tuples_on NAT st t1 = t * P holds
prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
let t1 be FinSequence of 3 -tuples_on NAT; :: thesis: ( t1 = t * P implies prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P )
A1: rng P = dom t by FUNCT_2:def 3;
assume A2: t1 = t * P ; :: thesis: prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
then A3: dom P = dom t1 by A1, RELAT_1:27;

A4: now :: thesis: for x being object st x in dom t1 holds
(prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . x

let x be object ; :: thesis: ( x in dom t1 implies (prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . x )
assume A5: x in dom t1 ; :: thesis: (prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . x
then reconsider i = x as Element of NAT ;
A6: ( (prodTuples (p,q,r,t1)) . i = ((p . ((t1 /. i) /. 1)) * (q . ((t1 /. i) /. 2))) * (r . ((t1 /. i) /. 3)) & ((prodTuples (p,q,r,t)) * P) . x = (prodTuples (p,q,r,t)) . (P . x) ) by A3, A5, Def5, FUNCT_1:13;
reconsider j = P . i as Element of NAT ;
A7: P . i in rng P by A3, A5, FUNCT_1:def 3;
t1 /. i = t1 . i by A5, PARTFUN1:def 6
.= t . (P . i) by A2, A5, FUNCT_1:12
.= t /. j by A1, A7, PARTFUN1:def 6 ;
hence (prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . x by A1, A7, A6, Def5; :: thesis: verum

end;

len (prodTuples (p,q,r,t1)) = len t1 by Def5;
then A8: dom (prodTuples (p,q,r,t1)) = Seg (len t1) by FINSEQ_1:def 3;
len (prodTuples (p,q,r,t)) = len t by Def5;
then rng P = dom (prodTuples (p,q,r,t)) by A1, FINSEQ_3:29;
then A9: dom ((prodTuples (p,q,r,t)) * P) = dom t1 by A3, RELAT_1:27;
dom t1 = Seg (len t1) by FINSEQ_1:def 3;
hence prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P by A8, A9, A4, FUNCT_1:2; :: thesis: verum