let f1, f2, g1, g2, h1, h2 be complex-valued FinSequence; :: thesis: ( len f1 = len g1 & len g1 = len h1 implies ((f1 ^ f2) (#) (g1 ^ g2)) (#) (h1 ^ h2) = ((f1 (#) g1) (#) h1) ^ ((f2 (#) g2) (#) h2) )
assume that
A1: len f1 = len g1 and
A2: len g1 = len h1 ; :: thesis: ((f1 ^ f2) (#) (g1 ^ g2)) (#) (h1 ^ h2) = ((f1 (#) g1) (#) h1) ^ ((f2 (#) g2) (#) h2)
A3: (f1 ^ f2) (#) (g1 ^ g2) = (f1 (#) g1) ^ (f2 (#) g2) by A1, EULRPART:8;
len (f1 (#) g1) = min ((len f1),(len g1)) by INT_6:3;
hence ((f1 ^ f2) (#) (g1 ^ g2)) (#) (h1 ^ h2) = ((f1 (#) g1) (#) h1) ^ ((f2 (#) g2) (#) h2) by A1, A2, A3, EULRPART:8; :: thesis: verum