let D, D9, E be non empty set ; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))

A0: ( i is Nat & j is Nat ) by TARSKI:1;

defpred S_{1}[ 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));

_{1}[j] holds

S_{1}[j + 1]
;

_{1}[ 0 ]
;

for j being Nat holds S_{1}[j]
from NAT_1:sch 2(A8, A6);

hence F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) by A0; :: thesis: verum

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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9))

A0: ( i is Nat & j is Nat ) by TARSKI:1;

defpred S

for S9 being Tuple of $1,D9 holds F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9));

now :: thesis: 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))

then A6:
for j being Nat st Sfor 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 ; :: thesis: ( ( 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)) ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: verum

end;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)) ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: verum

S

now :: thesis: 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))

then A8:
Sfor 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; :: thesis: 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; :: thesis: 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; :: thesis: verum

end;let S9 be Tuple of 0 ,D9; :: thesis: 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; :: thesis: verum

for j being Nat holds S

hence F .: ((T ^ S),(T9 ^ S9)) = (F .: (T,T9)) ^ (F .: (S,S9)) by A0; :: thesis: verum