let n, m, k be Nat; :: thesis: for K being Field
for A being Matrix of n,m,K
for B being Matrix of n,k,K
for P being Function of (Seg n),(Seg n) holds
( Solutions_of A,B c= Solutions_of (A * P),(B * P) & ( P is one-to-one implies Solutions_of A,B = Solutions_of (A * P),(B * P) ) )
let K be Field; :: thesis: for A being Matrix of n,m,K
for B being Matrix of n,k,K
for P being Function of (Seg n),(Seg n) holds
( Solutions_of A,B c= Solutions_of (A * P),(B * P) & ( P is one-to-one implies Solutions_of A,B = Solutions_of (A * P),(B * P) ) )
set IDn = idseq n;
( len (idseq n) = n & idseq n is FinSequence of NAT ) by FINSEQ_1:def 18, FINSEQ_2:52;
then reconsider IDn = idseq n as Element of n -tuples_on NAT by FINSEQ_2:110;
let A be Matrix of n,m,K; :: thesis: for B being Matrix of n,k,K
for P being Function of (Seg n),(Seg n) holds
( Solutions_of A,B c= Solutions_of (A * P),(B * P) & ( P is one-to-one implies Solutions_of A,B = Solutions_of (A * P),(B * P) ) )
let B be Matrix of n,k,K; :: thesis: for P being Function of (Seg n),(Seg n) holds
( Solutions_of A,B c= Solutions_of (A * P),(B * P) & ( P is one-to-one implies Solutions_of A,B = Solutions_of (A * P),(B * P) ) )
let P be Function of (Seg n),(Seg n); :: thesis: ( Solutions_of A,B c= Solutions_of (A * P),(B * P) & ( P is one-to-one implies Solutions_of A,B = Solutions_of (A * P),(B * P) ) )
A1: rng P c= Seg n by RELAT_1:def 19;
dom IDn = Seg n by FUNCT_2:67;
then reconsider IDnP = IDn * P as FinSequence of NAT by FINSEQ_2:51;
dom P = Seg n by FUNCT_2:67;
then ( n in NAT & dom IDnP = Seg n ) by A1, ORDINAL1:def 13, RELAT_1:79;
then len IDnP = n by FINSEQ_1:def 3;
then reconsider IDnP = IDnP as Element of n -tuples_on NAT by FINSEQ_2:110;
A2: n = len A by MATRIX_1:def 3;
A3: (idseq n) * P = P by A1, RELAT_1:79;
then A4: rng IDnP c= dom A by A1, A2, FINSEQ_1:def 3;
A5: ( IDn = Sgm (Seg n) & card (Seg n) = n ) by FINSEQ_1:78, FINSEQ_3:54;
then A6: Segm A,IDnP,(Sgm (Seg (width A))) = (Segm A,(Seg (len A)),(Seg (width A))) * P by A2, MATRIX13:33
.= A * P by MATRIX13:46 ;
A7: len B = n by MATRIX_1:def 3;
then A8: Segm B,IDnP,(Sgm (Seg (width B))) = (Segm B,(Seg (len B)),(Seg (width B))) * P by A5, MATRIX13:33
.= B * P by MATRIX13:46 ;

per cases ( n > 0 or n = 0 ) ;

suppose A9: n > 0 ; :: thesis: ( Solutions_of A,B c= Solutions_of (A * P),(B * P) & ( P is one-to-one implies Solutions_of A,B = Solutions_of (A * P),(B * P) ) )

hence Solutions_of A,B c= Solutions_of (A * P),(B * P) by A6, A8, A4, Th42; :: thesis: ( P is one-to-one implies Solutions_of A,B = Solutions_of (A * P),(B * P) )
A10: card (Seg n) = card (Seg n) ;
A11: dom A = Seg n by A2, FINSEQ_1:def 3;
A12: dom B = Seg n by A7, FINSEQ_1:def 3;
assume P is one-to-one ; :: thesis: Solutions_of A,B = Solutions_of (A * P),(B * P)
then P is onto by A10, STIRL2_1:70;
then rng P = Seg n by FUNCT_2:def 3;
then for i being Nat st i in (dom A) \ (rng IDnP) holds
( Line A,i = (width A) |-> (0. K) & Line B,i = (width B) |-> (0. K) ) by A3, A11, XBOOLE_1:37;
hence Solutions_of A,B = Solutions_of (A * P),(B * P) by A1, A3, A6, A8, A9, A11, A12, Th43; :: thesis: verum

end;

suppose A13: n = 0 ; :: thesis: ( Solutions_of A,B c= Solutions_of (A * P),(B * P) & ( P is one-to-one implies Solutions_of A,B = Solutions_of (A * P),(B * P) ) )

then len B = 0 by MATRIX_1:23;
then A14: B = {} ;
len A = 0 by A13, MATRIX_1:23;
then A15: A = {} ;
A * P = {} by A13;
hence ( Solutions_of A,B c= Solutions_of (A * P),(B * P) & ( P is one-to-one implies Solutions_of A,B = Solutions_of (A * P),(B * P) ) ) by A15, A14; :: thesis: verum

end;

end;