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 )
assume A1:
t1 = t * P
; :: thesis: prodTuples p,q,r,t1 = (prodTuples p,q,r,t) * P
len (prodTuples p,q,r,t1) = len t1
by Def5;
then A2:
dom (prodTuples p,q,r,t1) = Seg (len t1)
by FINSEQ_1:def 3;
A3:
rng P = dom t
by FUNCT_2:def 3;
len (prodTuples p,q,r,t) = len t
by Def5;
then A4:
rng P = dom (prodTuples p,q,r,t)
by A3, FINSEQ_3:31;
A5:
dom P = dom t1
by A1, A3, RELAT_1:46;
then A6:
dom ((prodTuples p,q,r,t) * P) = dom t1
by A4, RELAT_1:46;
A7:
dom t1 = Seg (len t1)
by FINSEQ_1:def 3;
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 A8:
x in dom t1
;
:: thesis: (prodTuples p,q,r,t1) . x = ((prodTuples p,q,r,t) * P) . xthen reconsider i =
x as
Element of
NAT ;
A9:
P . i in rng P
by A5, A8, FUNCT_1:def 5;
reconsider j =
P . i as
Element of
NAT ;
A10:
(prodTuples p,q,r,t1) . i = ((p . ((t1 /. i) /. 1)) * (q . ((t1 /. i) /. 2))) * (r . ((t1 /. i) /. 3))
by A8, Def5;
A11:
((prodTuples p,q,r,t) * P) . x = (prodTuples p,q,r,t) . (P . x)
by A5, A8, FUNCT_1:23;
t1 /. i =
t1 . i
by A8, PARTFUN1:def 8
.=
t . (P . i)
by A1, A8, FUNCT_1:22
.=
t /. j
by A3, A9, PARTFUN1:def 8
;
hence
(prodTuples p,q,r,t1) . x = ((prodTuples p,q,r,t) * P) . x
by A3, A9, A10, A11, Def5;
:: thesis: verum end;
hence
prodTuples p,q,r,t1 = (prodTuples p,q,r,t) * P
by A2, A6, A7, FUNCT_1:9; :: thesis: verum