let input be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: InvShiftRows . (ShiftRows . input) = input
InvShiftRows . (ShiftRows . input) in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then P3: ex s being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( InvShiftRows . (ShiftRows . input) = s & len s = 4 ) ;
input in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then P4: ex s being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( input = s & len s = 4 ) ;

now :: thesis: for i being Nat st 1 <= i & i <= len (InvShiftRows . (ShiftRows . input)) holds
(InvShiftRows . (ShiftRows . input)) . i = input . i

let i be Nat; :: thesis: ( 1 <= i & i <= len (InvShiftRows . (ShiftRows . input)) implies (InvShiftRows . (ShiftRows . input)) . i = input . i )
assume ( 1 <= i & i <= len (InvShiftRows . (ShiftRows . input)) ) ; :: thesis: (InvShiftRows . (ShiftRows . input)) . i = input . i
then XX2: i in Seg 4 by P3;
then consider xi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) such that
XX3: ( xi = input . i & (ShiftRows . input) . i = Op-Shift (xi,(5 - i)) ) by DefShiftRows;
xi in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then YY1: ex s being Element of (8 -tuples_on BOOLEAN) * st
( xi = s & len s = 4 ) ;
consider yi being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) such that
XX4: ( yi = (ShiftRows . input) . i & (InvShiftRows . (ShiftRows . input)) . i = Op-Shift (yi,(i - 1)) ) by DefInvShiftRows, XX2;
thus (InvShiftRows . (ShiftRows . input)) . i = Op-Shift (xi,((5 - i) + (i - 1))) by XX3, XX4, DESCIP_1:10, YY1
.= input . i by DESCIP_1:12, YY1, XX3 ; :: thesis: verum

end;

hence InvShiftRows . (ShiftRows . input) = input by P3, P4, FINSEQ_1:14; :: thesis: verum