let D, D9, E be non empty set ; for i, j being natural Number
for F being Function of [:D,D9:],E
for T being Tuple of i,D
for T9 being Tuple of i,D9
for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
let i, j be natural Number ; for F being Function of [:D,D9:],E
for T being Tuple of i,D
for T9 being Tuple of i,D9
for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
let F be Function of [:D,D9:],E; for T being Tuple of i,D
for T9 being Tuple of i,D9
for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
let T be Tuple of i,D; for T9 being Tuple of i,D9
for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
let T9 be Tuple of i,D9; for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
let S be Tuple of j,D; for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
let S9 be Tuple of j,D9; F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
A0:
( i is Nat & j is Nat )
by TARSKI:1;
defpred S1[ Nat] means for S being Tuple of $1,D
for S9 being Tuple of $1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9));
now for j being natural Number st ( for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) ) holds
for S being Tuple of j + 1,D
for S9 being Tuple of j + 1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))let j be
natural Number ;
( ( for S being Tuple of j,D
for S9 being Tuple of j,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) ) implies for S being Tuple of j + 1,D
for S9 being Tuple of j + 1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) )assume A1:
for
S being
Tuple of
j,
D for
S9 being
Tuple of
j,
D9 holds
F .: (
(T ^ S),
(T9 ^ S9))
= (F .: (T,T9)) ^ (F .: (S,S9))
;
for S being Tuple of j + 1,D
for S9 being Tuple of j + 1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))let S be
Tuple of
j + 1,
D;
for S9 being Tuple of j + 1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))let S9 be
Tuple of
j + 1,
D9;
F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))consider S1 being
Element of
j -tuples_on D,
d being
Element of
D such that A2:
S = S1 ^ <*d*>
by FINSEQ_2:117;
A3:
T ^ S = (T ^ S1) ^ <*d*>
by A2, FINSEQ_1:32;
reconsider S1 =
S1 as
Tuple of
j,
D ;
consider S19 being
Element of
j -tuples_on D9,
d9 being
Element of
D9 such that A4:
S9 = S19 ^ <*d9*>
by FINSEQ_2:117;
A5:
T9 ^ S9 = (T9 ^ S19) ^ <*d9*>
by A4, FINSEQ_1:32;
reconsider S19 =
S19 as
Tuple of
j,
D9 ;
thus F .: (
(T ^ S),
(T9 ^ S9)) =
(F .: ((T ^ S1),(T9 ^ S19))) ^ <*(F . (d,d9))*>
by A3, A5, Th10
.=
((F .: (T,T9)) ^ (F .: (S1,S19))) ^ <*(F . (d,d9))*>
by A1
.=
(F .: (T,T9)) ^ ((F .: (S1,S19)) ^ <*(F . (d,d9))*>)
by FINSEQ_1:32
.=
(F .: (T,T9)) ^ (F .: (S,S9))
by A2, A4, Th10
;
verum end;
then A6:
for j being Nat st S1[j] holds
S1[j + 1]
;
now for S being Tuple of 0 ,D
for S9 being Tuple of 0 ,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))let S be
Tuple of
0 ,
D;
for S9 being Tuple of 0 ,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))let S9 be
Tuple of
0 ,
D9;
F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
S = <*> D
;
then A7:
F .: (
S,
S9)
= <*> E
by FINSEQ_2:73;
(
T ^ S = T &
T9 ^ S9 = T9 )
by FINSEQ_2:95;
hence
F .: (
(T ^ S),
(T9 ^ S9))
= (F .: (T,T9)) ^ (F .: (S,S9))
by A7, FINSEQ_1:34;
verum end;
then A8:
S1[ 0 ]
;
for j being Nat holds S1[j]
from NAT_1:sch 2(A8, A6);
hence
F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))
by A0; verum