let k, m, n 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 CARD_1:def 7, FINSEQ_2:48;
then reconsider IDn = idseq n as Element of n -tuples_on NAT by FINSEQ_2:92;
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 ;
then reconsider IDnP = IDn * P as FinSequence of NAT by FINSEQ_2:47;
dom P = Seg n by FUNCT_2:52;
then ( n in NAT & dom IDnP = Seg n ) by A1, ORDINAL1:def 12, RELAT_1:53;
then len IDnP = n by FINSEQ_1:def 3;
then reconsider IDnP = IDnP as Element of n -tuples_on NAT by FINSEQ_2:92;
A2: n = len A by MATRIX_0:def 2;
A3: (idseq n) * P = P by A1, RELAT_1:53;
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:57, FINSEQ_3:48;
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_0:def 2;
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, FINSEQ_4:63;
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_0:22;
then A14: B = {} ;
len A = 0 by A13, MATRIX_0:22;
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;