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 ;
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 ;
reconsider j = P . i as Element of NAT ;
A7: P . i in rng P by ;
t1 /. i = t1 . i by
.= t . (P . i) by
.= t /. j by ;
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 ;
then A9: dom ((prodTuples (p,q,r,t)) * P) = dom t1 by ;
dom t1 = Seg (len t1) by FINSEQ_1:def 3;
hence prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P by ; :: thesis: verum