let D be non empty set ; :: thesis: for x being Element of 4 -tuples_on (4 -tuples_on D)
for k being Element of NAT st k in Seg 4 holds
ex x1, x2, x3, x4 being Element of D st
( x1 = (x . k) . 1 & x2 = (x . k) . 2 & x3 = (x . k) . 3 & x4 = (x . k) . 4 )
let x be Element of 4 -tuples_on (4 -tuples_on D); :: thesis: for k being Element of NAT st k in Seg 4 holds
ex x1, x2, x3, x4 being Element of D st
( x1 = (x . k) . 1 & x2 = (x . k) . 2 & x3 = (x . k) . 3 & x4 = (x . k) . 4 )
let k be Element of NAT ; :: thesis: ( k in Seg 4 implies ex x1, x2, x3, x4 being Element of D st
( x1 = (x . k) . 1 & x2 = (x . k) . 2 & x3 = (x . k) . 3 & x4 = (x . k) . 4 ) )
assume AS: k in Seg 4 ; :: thesis: ex x1, x2, x3, x4 being Element of D st
( x1 = (x . k) . 1 & x2 = (x . k) . 2 & x3 = (x . k) . 3 & x4 = (x . k) . 4 )
x in 4 -tuples_on (4 -tuples_on D) ;
then ex s being Element of (4 -tuples_on D) * st
( x = s & len s = 4 ) ;
then k in dom x by AS, FINSEQ_1:def 3;
then x . k in rng x by FUNCT_1:3;
then x . k in 4 -tuples_on D ;
then Q13: ex s being Element of D * st
( x . k = s & len s = 4 ) ;
then reconsider xk = x . k as Element of D * ;
1 in Seg 4 ;
then 1 in dom xk by Q13, FINSEQ_1:def 3;
then xk . 1 in rng xk by FUNCT_1:3;
then reconsider x1 = xk . 1 as Element of D ;
2 in Seg 4 ;
then 2 in dom xk by Q13, FINSEQ_1:def 3;
then xk . 2 in rng xk by FUNCT_1:3;
then reconsider x2 = xk . 2 as Element of D ;
3 in Seg 4 ;
then 3 in dom xk by Q13, FINSEQ_1:def 3;
then xk . 3 in rng xk by FUNCT_1:3;
then reconsider x3 = xk . 3 as Element of D ;
4 in Seg 4 ;
then 4 in dom xk by Q13, FINSEQ_1:def 3;
then xk . 4 in rng xk by FUNCT_1:3;
then reconsider x4 = xk . 4 as Element of D ;
take x1 ; :: thesis: ex x2, x3, x4 being Element of D st
( x1 = (x . k) . 1 & x2 = (x . k) . 2 & x3 = (x . k) . 3 & x4 = (x . k) . 4 )
take x2 ; :: thesis: ex x3, x4 being Element of D st
( x1 = (x . k) . 1 & x2 = (x . k) . 2 & x3 = (x . k) . 3 & x4 = (x . k) . 4 )
take x3 ; :: thesis: ex x4 being Element of D st
( x1 = (x . k) . 1 & x2 = (x . k) . 2 & x3 = (x . k) . 3 & x4 = (x . k) . 4 )
take x4 ; :: thesis: ( x1 = (x . k) . 1 & x2 = (x . k) . 2 & x3 = (x . k) . 3 & x4 = (x . k) . 4 )
thus ( x1 = (x . k) . 1 & x2 = (x . k) . 2 & x3 = (x . k) . 3 & x4 = (x . k) . 4 ) ; :: thesis: verum