let n, m be Nat; :: thesis: for D being non empty set
for A, B being Matrix of n,m,D
for i being Nat st i <= n & 0 < n holds
for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
let D be non empty set ; :: thesis: for A, B being Matrix of n,m,D
for i being Nat st i <= n & 0 < n holds
for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
let A, B be Matrix of n,m,D; :: thesis: for i being Nat st i <= n & 0 < n holds
for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
let i be Nat; :: thesis: ( i <= n & 0 < n implies for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) ) )
assume that
A1: i <= n and
A2: 0 < n ; :: thesis: for F being Function of (Seg i),(Seg n) ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
set I = idseq n;
let F be Function of (Seg i),(Seg n); :: thesis: ex M being Matrix of n,m,D st
( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
set IF = (idseq n) +* F;
A3: dom (idseq n) = Seg n ;
A4: rng (idseq n) = Seg n ;
rng F c= Seg n by RELAT_1:def 19;
then (rng F) \/ (Seg n) = Seg n by XBOOLE_1:12;
then A5: rng ((idseq n) +* F) c= Seg n by A4, FUNCT_4:17;
A6: Seg i c= Seg n by A1, FINSEQ_1:5;
then A7: (Seg i) \/ (Seg n) = Seg n by XBOOLE_1:12;
A8: dom F = Seg i by A2, FUNCT_2:def 1;
then dom F c= Seg n by A1, FINSEQ_1:5;
then (dom F) \/ (Seg n) = Seg n by XBOOLE_1:12;
then dom ((idseq n) +* F) = Seg n by A3, FUNCT_4:def 1;
then reconsider IF = (idseq n) +* F as Function of (Seg n),(Seg n) by A5, FUNCT_2:2;
reconsider BIF = B * IF as Matrix of n,m,D ;
set BIFi = BIF | (Seg i);
set M = A +* (BIF | (Seg i));
A9: len B = n by A2, MATRIX_0:23;
len BIF = len B by Def4;
then dom BIF = Seg n by A9, FINSEQ_1:def 3;
then A10: dom (BIF | (Seg i)) = Seg i by A6, RELAT_1:62;
len A = n by A2, MATRIX_0:23;
then dom A = Seg n by FINSEQ_1:def 3;
then A11: dom (A +* (BIF | (Seg i))) = (Seg i) \/ (Seg n) by A10, FUNCT_4:def 1;
then reconsider M = A +* (BIF | (Seg i)) as FinSequence by A7, FINSEQ_1:def 2;
A12: for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) )

proof

let j be Nat; :: thesis: ( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) )
thus ( j in Seg i implies M . j = B . (F . j) ) :: thesis: ( not j in Seg i implies M . j = A . j )

proof

A13: Seg i c= Seg n by A1, FINSEQ_1:5;
assume A14: j in Seg i ; :: thesis: M . j = B . (F . j)
then A15: (BIF | (Seg i)) . j = BIF . j by A10, FUNCT_1:47;
IF . j = F . j by A8, A14, FUNCT_4:13;
then A16: Line (BIF,j) = B . (F . j) by A14, A13, Th38;
Line (BIF,j) = BIF . j by A14, A13, MATRIX_0:52;
hence M . j = B . (F . j) by A10, A14, A16, A15, FUNCT_4:13; :: thesis: verum

end;

assume not j in Seg i ; :: thesis: M . j = A . j
hence M . j = A . j by A10, FUNCT_4:11; :: thesis: verum

end;

A17: for x being object st x in rng M holds
ex p being FinSequence of D st
( x = p & len p = m )

proof

let x be object ; :: thesis: ( x in rng M implies ex p being FinSequence of D st
( x = p & len p = m ) )
assume x in rng M ; :: thesis: ex p being FinSequence of D st
( x = p & len p = m )
then consider k being object such that
A18: k in dom M and
A19: M . k = x by FUNCT_1:def 3;
reconsider k = k as Nat by A18;

per cases ( k in Seg i or not k in Seg i ) ;

suppose A20: k in Seg i ; :: thesis: ex p being FinSequence of D st
( x = p & len p = m )

A21: rng F c= Seg n by RELAT_1:def 19;
A22: F . k in rng F by A8, A20, FUNCT_1:def 3;
then reconsider Fk = F . k as Element of NAT by A21, TARSKI:def 3;
take L = Line (B,Fk); :: thesis: ( x = L & len L = m )
A23: len L = width B by MATRIX_0:def 7;
B . (F . k) = L by A22, A21, MATRIX_0:52;
hence ( x = L & len L = m ) by A2, A12, A19, A20, A23, MATRIX_0:23; :: thesis: verum

end;

suppose A24: not k in Seg i ; :: thesis: ex p being FinSequence of D st
( x = p & len p = m )

take L = Line (A,k); :: thesis: ( x = L & len L = m )
A25: len L = width A by MATRIX_0:def 7;
M . k = A . k by A12, A24;
hence ( x = L & len L = m ) by A2, A11, A7, A18, A19, A25, MATRIX_0:23, MATRIX_0:52; :: thesis: verum

end;

end;

end;

then reconsider M = M as Matrix of D by MATRIX_0:9;
n is Element of NAT by ORDINAL1:def 12;
then A26: len M = n by A11, A7, FINSEQ_1:def 3;

now :: thesis: for p being FinSequence of D st p in rng M holds
len p = m

let p be FinSequence of D; :: thesis: ( p in rng M implies len p = m )
assume p in rng M ; :: thesis: len p = m
then ex q being FinSequence of D st
( p = q & len q = m ) by A17;
hence len p = m ; :: thesis: verum

end;

then reconsider M = M as Matrix of n,m,D by A26, MATRIX_0:def 2;
take M ; :: thesis: ( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) )
thus ( M = A +* ((B * ((idseq n) +* F)) | (Seg i)) & ( for j being Nat holds
( ( j in Seg i implies M . j = B . (F . j) ) & ( not j in Seg i implies M . j = A . j ) ) ) ) by A12; :: thesis: verum