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:46;

A4: now

let x be set ; :: 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:23;
reconsider j = P . i as Element of NAT ;
A7: P . i in rng P by A3, A5, FUNCT_1:def 5;
t1 /. i = t1 . i by A5, PARTFUN1:def 8
.= t . (P . i) by A2, A5, FUNCT_1:22
.= t /. j by A1, A7, PARTFUN1:def 8 ;
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:31;
then A9: dom ((prodTuples p,q,r,t) * P) = dom t1 by A3, RELAT_1:46;
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:9; :: thesis: verum