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 )
reconsider q1 = p1, q2 = p2 as Element of D * by FINSEQ_1:def 11;
reconsider M = <*q1,q2*> as FinSequence of D * ;
assume A1: ( len p1 = n & len p2 = n ) ; :: thesis: <*p1,p2*> is Matrix of 2,n,D
then reconsider M = M as Matrix of D by Th4;
M is 2,n -size

proof

thus len M = 2 by FINSEQ_1:44; :: according to MATRIX_0:def 2 :: 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:127;
hence len r = n by A1, TARSKI:def 2; :: thesis: verum

end;

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