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) ) )
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) ) )
set IDn = idseq n;
( len (idseq n) = n & idseq n is FinSequence of NAT ) by FINSEQ_2:52, FINSEQ_1:def 18;
then reconsider IDn = idseq n as Element of n -tuples_on NAT by FINSEQ_2:110;
A1: ( dom IDn = Seg n & rng P c= Seg n & dom P = Seg n ) by FUNCT_2:67, RELAT_1:def 19;
then reconsider IDnP = IDn * P as FinSequence of NAT by FINSEQ_2:51;
A2: n in NAT by ORDINAL1:def 13;
dom IDnP = Seg n by A1, RELAT_1:79;
then len IDnP = n by A2, FINSEQ_1:def 3;
then reconsider IDnP = IDnP as Element of n -tuples_on NAT by FINSEQ_2:110;
A3: ( IDn = Sgm (Seg n) & n = len A & len B = n & card (Seg n) = n & (idseq n) * P = P ) by A1, FINSEQ_1:78, FINSEQ_3:54, MATRIX_1:def 3, RELAT_1:79;
then A4: Segm A,IDnP,(Sgm (Seg (width A))) = (Segm A,(Seg (len A)),(Seg (width A))) * P by MATRIX13:33
.= A * P by MATRIX13:46 ;
A5: Segm B,IDnP,(Sgm (Seg (width B))) = (Segm B,(Seg (len B)),(Seg (width B))) * P by A3, MATRIX13:33
.= B * P by MATRIX13:46 ;
A6: rng IDnP c= dom A by A1, A3, FINSEQ_1:def 3;

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

suppose A7: 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 A4, A5, A6, Th42; :: thesis: ( P is one-to-one implies Solutions_of A,B = Solutions_of (A * P),(B * P) )
assume A8: P is one-to-one ; :: thesis: Solutions_of A,B = Solutions_of (A * P),(B * P)
card (Seg n) = card (Seg n) ;
then P is onto by A8, STIRL2_1:70;
then A9: rng P = Seg n by FUNCT_2:def 3;
A10: ( dom A = Seg n & dom B = Seg n ) by A3, FINSEQ_1: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, A9, XBOOLE_1:37;
hence Solutions_of A,B = Solutions_of (A * P),(B * P) by A4, A5, Th43, A1, A3, A7, A10; :: thesis: verum

end;

suppose 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 A = 0 & len B = 0 & len (A * P) = 0 & len (B * P) = 0 ) by MATRIX_1:23;
then ( A = {} & B = {} & A * P = {} & B * P = {} ) ;
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) ) ) ; :: thesis: verum

end;

end;