let E, D, D' be non empty set ; :: thesis: for i, j being Nat
for F being Function of [:D,D':],E
for T being Tuple of ,D
for T' being Tuple of ,D'
for S being Tuple of ,D
for S' being Tuple of ,D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let i, j be Nat; :: thesis: for F being Function of [:D,D':],E
for T being Tuple of ,D
for T' being Tuple of ,D'
for S being Tuple of ,D
for S' being Tuple of ,D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let F be Function of [:D,D':],E; :: thesis: for T being Tuple of ,D
for T' being Tuple of ,D'
for S being Tuple of ,D
for S' being Tuple of ,D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let T be Tuple of ,D; :: thesis: for T' being Tuple of ,D'
for S being Tuple of ,D
for S' being Tuple of ,D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let T' be Tuple of ,D'; :: thesis: for S being Tuple of ,D
for S' being Tuple of ,D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let S be Tuple of ,D; :: thesis: for S' being Tuple of ,D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
let S' be Tuple of ,D'; :: thesis: F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
defpred S1[ Nat] means for S being Tuple of ,D
for S' being Tuple of ,D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S');
now let j be
Nat;
:: thesis: ( ( for S being Tuple of ,D
for S' being Tuple of ,D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S') ) implies for S being Tuple of ,D
for S' being Tuple of ,D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S') )assume A1:
for
S being
Tuple of ,
D for
S' being
Tuple of ,
D' holds
F .: (T ^ S),
(T' ^ S') = (F .: T,T') ^ (F .: S,S')
;
:: thesis: for S being Tuple of ,D
for S' being Tuple of ,D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')let S be
Tuple of ,
D;
:: thesis: for S' being Tuple of ,D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')let S' be
Tuple of ,
D';
:: thesis: F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')consider S1 being
Element of
j -tuples_on D,
d being
Element of
D such that A2:
S = S1 ^ <*d*>
by FINSEQ_2:137;
A3:
T ^ S = (T ^ S1) ^ <*d*>
by A2, FINSEQ_1:45;
reconsider S1 =
S1 as
Tuple of ,
D by FINSEQ_2:151;
consider S1' being
Element of
j -tuples_on D',
d' being
Element of
D' such that A4:
S' = S1' ^ <*d'*>
by FINSEQ_2:137;
A5:
T' ^ S' = (T' ^ S1') ^ <*d'*>
by A4, FINSEQ_1:45;
reconsider S1' =
S1' as
Tuple of ,
D' by FINSEQ_2:151;
(
T ^ S1 is
Tuple of ,
D &
T' ^ S1' is
Tuple of ,
D' )
by FINSEQ_2:127;
hence F .: (T ^ S),
(T' ^ S') =
(F .: (T ^ S1),(T' ^ S1')) ^ <*(F . d,d')*>
by A3, A5, Th11
.=
((F .: T,T') ^ (F .: S1,S1')) ^ <*(F . d,d')*>
by A1
.=
(F .: T,T') ^ ((F .: S1,S1') ^ <*(F . d,d')*>)
by FINSEQ_1:45
.=
(F .: T,T') ^ (F .: S,S')
by A2, A4, Th11
;
:: thesis: verum end;
then A6:
for j being Nat st S1[j] holds
S1[j + 1]
;
now let S be
Tuple of ,
D;
:: thesis: for S' being Tuple of ,D' holds F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')let S' be
Tuple of ,
D';
:: thesis: F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
S = <*> D
;
then A7:
F .: S,
S' = <*> E
by FINSEQ_2:87;
(
T ^ S = T &
T' ^ S' = T' )
by FINSEQ_2:115;
hence
F .: (T ^ S),
(T' ^ S') = (F .: T,T') ^ (F .: S,S')
by A7, FINSEQ_1:47;
:: thesis: verum end;
then A8:
S1[ 0 ]
;
for j being Nat holds S1[j]
from NAT_1:sch 2(A8, A6);
hence
F .: (T ^ S),(T' ^ S') = (F .: T,T') ^ (F .: S,S')
; :: thesis: verum