let n be Nat; 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 ; 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; ( 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 )
; <*p1,p2*> is Matrix of 2,n,D
then reconsider M = M as Matrix of D by Th4;
M is 2,n -size
hence
<*p1,p2*> is Matrix of 2,n,D
; verum