let D be non empty set ; :: thesis: for n being 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 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 )
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 * ;
assume A1: ( len p1 = n & len p2 = n & len p3 = n ) ; :: thesis: <*p1,p2,p3*> is Matrix of 3,n,D
then reconsider M = M as Matrix of D by Th33;
M is 3,n -size
proof
thus len M = 3 by FINSEQ_1:45; :: according to MATRIX_0:def 2 :: thesis: for b1 being FinSequence of D holds
( not b1 in rng M or len b1 = 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:128;
hence len r = n by A1, ENUMSET1:def 1; :: thesis: verum
end;
hence <*p1,p2,p3*> is Matrix of 3,n,D ; :: thesis: verum