let f1, f2, g1, g2 be complex-valued FinSequence; :: thesis: ( len f1 = len g1 implies (f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2) )
assume A1: len f1 = len g1 ; :: thesis: (f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2)
( len f2 <= len g2 or len f2 >= len g2 ) ;
hence (f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2) by A1, Lm1; :: thesis: verum