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

proof

thus len M = 2 by FINSEQ_1:61; :: according to MATRIX_1:def 3 :: thesis: for p being FinSequence of D st p in rng M holds
len p = n
let r be FinSequence of D; :: thesis: ( r in rng M implies len r = n )
assume r in rng M ; :: thesis: len r = n
then r in {p1,p2} by FINSEQ_2:147;
hence len r = n by A1, A2, TARSKI:def 2; :: thesis: verum

end;

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