let L be non empty multMagma ; 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; 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; 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); 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; ( 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
; prodTuples (p,q,r,t1) = (prodTuples (p,q,r,t)) * P
then A3:
dom P = dom t1
by A1, RELAT_1:27;
A4:
now for x being object st x in dom t1 holds
(prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . xlet x be
object ;
( x in dom t1 implies (prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . x )assume A5:
x in dom t1
;
(prodTuples (p,q,r,t1)) . x = ((prodTuples (p,q,r,t)) * P) . xthen 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;
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; verum