let n be Nat; :: thesis: for K being Field
for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 is invertible holds
M1 * M2 is Idempotent
let K be Field; :: thesis: for M1, M2 being Matrix of n,K st M1 is Idempotent & M2 is Idempotent & M1 is invertible holds
M1 * M2 is Idempotent
let M1, M2 be Matrix of n,K; :: thesis: ( M1 is Idempotent & M2 is Idempotent & M1 is invertible implies M1 * M2 is Idempotent )
assume A1: ( M1 is Idempotent & M2 is Idempotent & M1 is invertible ) ; :: thesis: M1 * M2 is Idempotent
then ( M2 * M2 = M2 & M1 = 1. K,n ) by Def1, Th10;
hence M1 * M2 is Idempotent by A1, MATRIX_3:20; :: thesis: verum