let K1, K2 be Matrix of K; :: thesis: ( len K1 = len b1 & ( for k being Nat st k in dom b1 holds
K1 /. k = (f . (b1 /. k)) |-- b2 ) & len K2 = len b1 & ( for k being Nat st k in dom b1 holds
K2 /. k = (f . (b1 /. k)) |-- b2 ) implies K1 = K2 )
assume that
A10: len K1 = len b1 and
A11: for k being Nat st k in dom b1 holds
K1 /. k = (f . (b1 /. k)) |-- b2 and
A12: len K2 = len b1 and
A13: for k being Nat st k in dom b1 holds
K2 /. k = (f . (b1 /. k)) |-- b2 ; :: thesis: K1 = K2
for k being Nat st 1 <= k & k <= len K1 holds
K1 . k = K2 . k

proof

let k be Nat; :: thesis: ( 1 <= k & k <= len K1 implies K1 . k = K2 . k )
assume A14: ( 1 <= k & k <= len K1 ) ; :: thesis: K1 . k = K2 . k
then A15: k in dom b1 by A10, FINSEQ_3:25;
A16: k in dom K2 by A10, A12, A14, FINSEQ_3:25;
k in dom K1 by A14, FINSEQ_3:25;
hence K1 . k = K1 /. k by PARTFUN1:def 6
.= (f . (b1 /. k)) |-- b2 by A11, A15
.= K2 /. k by A13, A15
.= K2 . k by A16, PARTFUN1:def 6 ;
:: thesis: verum

end;

hence K1 = K2 by A10, A12, FINSEQ_1:14; :: thesis: verum