let U1 be Universal_Algebra; :: thesis: for a being FinSequence of U1 holds (id the carrier of U1) * a = a
let a be FinSequence of U1; :: thesis: (id the carrier of U1) * a = a
set f = id the carrier of U1;
A1: dom ((id the carrier of U1) * a) = dom a by FINSEQ_3:120;
A2: now :: thesis: for n being Nat st n in dom ((id the carrier of U1) * a) holds
((id the carrier of U1) * a) . n = a . n
let n be Nat; :: thesis: ( n in dom ((id the carrier of U1) * a) implies ((id the carrier of U1) * a) . n = a . n )
assume A3: n in dom ((id the carrier of U1) * a) ; :: thesis: ((id the carrier of U1) * a) . n = a . n
then reconsider u = a . n as Element of U1 by A1, FINSEQ_2:11;
(id the carrier of U1) . u = u ;
hence ((id the carrier of U1) * a) . n = a . n by A3, FINSEQ_3:120; :: thesis: verum
end;
len ((id the carrier of U1) * a) = len a by FINSEQ_3:120;
hence (id the carrier of U1) * a = a by A2, FINSEQ_2:9; :: thesis: verum