let D be non empty set ; :: thesis: for n being Element of NAT
for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds
<*p1,p2,p3*> is Matrix of 3,n,D
let n be Element of NAT ; :: thesis: for p1, p2, p3 being FinSequence of D st len p1 = n & len p2 = n & len p3 = n holds
<*p1,p2,p3*> is Matrix of 3,n,D
let p1, p2, p3 be FinSequence of D; :: thesis: ( len p1 = n & len p2 = n & len p3 = n implies <*p1,p2,p3*> is Matrix of 3,n,D )
assume that
A1: len p1 = n and
A2: len p2 = n and
A3: len p3 = n ; :: thesis: <*p1,p2,p3*> is Matrix of 3,n,D
reconsider q1 = p1, q2 = p2, q3 = p3 as Element of D * by FINSEQ_1:def 11;
reconsider M = <*q1,q2,q3*> as FinSequence of D * ;
reconsider M = M as Matrix of D by A1, A2, A3, Th33;
M is Matrix of 3,n,D

proof

thus len M = 3 by FINSEQ_1:62; :: according to MATRIX_1:def 3 :: thesis: for b₁ being FinSequence of D holds
( not b₁ in rng M or len b₁ = n )
let r be FinSequence of D; :: thesis: ( not r in rng M or len r = n )
assume r in rng M ; :: thesis: len r = n
then r in {p1,p2,p3} by FINSEQ_2:148;
hence len r = n by A1, A2, A3, ENUMSET1:def 1; :: thesis: verum

end;

hence <*p1,p2,p3*> is Matrix of 3,n,D ; :: thesis: verum