let n be Nat; :: thesis: for K being Field
for M1 being Matrix of n,K st n > 0 holds
( M1 is Idempotent iff M1 @ is Idempotent )
let K be Field; :: thesis: for M1 being Matrix of n,K st n > 0 holds
( M1 is Idempotent iff M1 @ is Idempotent )
let M1 be Matrix of n,K; :: thesis: ( n > 0 implies ( M1 is Idempotent iff M1 @ is Idempotent ) )
assume A1: n > 0 ; :: thesis: ( M1 is Idempotent iff M1 @ is Idempotent )
set M2 = M1 @ ;
A2: ( width M1 = n & len M1 = n ) by MATRIX_1:25;
thus ( M1 is Idempotent implies M1 @ is Idempotent ) :: thesis: ( M1 @ is Idempotent implies M1 is Idempotent )

proof

assume A3: M1 is Idempotent ; :: thesis: M1 @ is Idempotent
(M1 @) * (M1 @) = (M1 * M1) @ by A1, A2, MATRIX_3:24
.= M1 @ by A3, Def1 ;
hence M1 @ is Idempotent by Def1; :: thesis: verum

end;

A4: ( width (M1 @) = n & len (M1 @) = n ) by MATRIX_1:25;
assume A5: M1 @ is Idempotent ; :: thesis: M1 is Idempotent
M1 = (M1 @) @ by A1, A2, MATRIX_2:15
.= ((M1 @) * (M1 @)) @ by A5, Def1
.= ((M1 @) @) * ((M1 @) @) by A1, A4, MATRIX_3:24
.= M1 * ((M1 @) @) by A1, A2, MATRIX_2:15
.= M1 * M1 by A1, A2, MATRIX_2:15 ;
hence M1 is Idempotent by Def1; :: thesis: verum