let K be non empty addLoopStr ; :: thesis: for f1, f2, g1, g2 being FinSequence of K st len f1 = len f2 holds
(f1 + f2) ^ (g1 + g2) = (f1 ^ g1) + (f2 ^ g2)
let f1, f2, g1, g2 be FinSequence of K; :: thesis: ( len f1 = len f2 implies (f1 + f2) ^ (g1 + g2) = (f1 ^ g1) + (f2 ^ g2) )
assume A1: len f1 = len f2 ; :: thesis: (f1 + f2) ^ (g1 + g2) = (f1 ^ g1) + (f2 ^ g2)
A2: ( dom (f1 + f2) = (dom f1) /\ (dom f2) & dom f1 = dom f2 & dom (g1 + g2) = (dom g1) /\ (dom g2) & dom ((f1 ^ g1) + (f2 ^ g2)) = (dom (f1 ^ g1)) /\ (dom (f2 ^ g2)) ) by A1, Lm1, FINSEQ_3:31;
then A3: len (f1 + f2) = len f1 by FINSEQ_3:31;
A4: ( dom g1 = Seg (len g1) & dom g2 = Seg (len g2) & dom (f1 ^ g1) = Seg ((len f1) + (len g1)) & dom (f2 ^ g2) = Seg ((len f2) + (len g2)) ) by FINSEQ_1:def 3, FINSEQ_1:def 7;

A5: now

per cases ( len g1 <= len g2 or len g1 > len g2 ) ;

suppose len g1 <= len g2 ; :: thesis: dom ((f1 + f2) ^ (g1 + g2)) = dom ((f1 ^ g1) + (f2 ^ g2))

then ( Seg (len g1) c= Seg (len g2) & (len f1) + (len g1) <= (len f2) + (len g2) ) by A1, FINSEQ_1:7, XREAL_1:9;
then ( dom (g1 + g2) = dom g1 & dom (f1 ^ g1) c= dom (f2 ^ g2) ) by A2, A4, FINSEQ_1:7, XBOOLE_1:28;
then ( len (g1 + g2) = len g1 & dom ((f1 ^ g1) + (f2 ^ g2)) = dom (f1 ^ g1) ) by A2, FINSEQ_3:31, XBOOLE_1:28;
hence dom ((f1 + f2) ^ (g1 + g2)) = dom ((f1 ^ g1) + (f2 ^ g2)) by A4, A3, FINSEQ_1:def 7; :: thesis: verum

end;

suppose len g1 > len g2 ; :: thesis: dom ((f1 + f2) ^ (g1 + g2)) = dom ((f1 ^ g1) + (f2 ^ g2))

then ( Seg (len g2) c= Seg (len g1) & (len f1) + (len g1) > (len f2) + (len g2) ) by A1, FINSEQ_1:7, XREAL_1:10;
then ( dom (g1 + g2) = dom g2 & dom (f2 ^ g2) c= dom (f1 ^ g1) ) by A2, A4, FINSEQ_1:7, XBOOLE_1:28;
then ( len (g1 + g2) = len g2 & dom ((f1 ^ g1) + (f2 ^ g2)) = dom (f2 ^ g2) ) by A2, FINSEQ_3:31, XBOOLE_1:28;
hence dom ((f1 + f2) ^ (g1 + g2)) = dom ((f1 ^ g1) + (f2 ^ g2)) by A1, A4, A3, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

now

let i be Nat; :: thesis: ( i in dom ((f1 + f2) ^ (g1 + g2)) implies ((f1 + f2) ^ (g1 + g2)) . i = ((f1 ^ g1) + (f2 ^ g2)) . i )
assume A6: i in dom ((f1 + f2) ^ (g1 + g2)) ; :: thesis: ((f1 + f2) ^ (g1 + g2)) . i = ((f1 ^ g1) + (f2 ^ g2)) . i

now

per cases ( i in dom (f1 + f2) or ex n being Nat st
( n in dom (g1 + g2) & i = (len (f1 + f2)) + n ) ) by A6, FINSEQ_1:38;

suppose A7: i in dom (f1 + f2) ; :: thesis: ((f1 + f2) ^ (g1 + g2)) . i = ((f1 ^ g1) + (f2 ^ g2)) . i

then A8: ( f1 /. i = f1 . i & f2 /. i = f2 . i ) by A2, PARTFUN1:def 8;
A9: ( f1 . i = (f1 ^ g1) . i & f2 . i = (f2 ^ g2) . i ) by A2, A7, FINSEQ_1:def 7;
thus ((f1 + f2) ^ (g1 + g2)) . i = (f1 + f2) . i by A7, FINSEQ_1:def 7
.= (f1 /. i) + (f2 /. i) by A7, A8, FVSUM_1:21
.= ((f1 ^ g1) + (f2 ^ g2)) . i by A5, A6, A8, A9, FVSUM_1:21 ; :: thesis: verum

end;

suppose ex n being Nat st
( n in dom (g1 + g2) & i = (len (f1 + f2)) + n ) ; :: thesis: ((f1 + f2) ^ (g1 + g2)) . i = ((f1 ^ g1) + (f2 ^ g2)) . i

then consider n being Nat such that
A10: ( n in dom (g1 + g2) & i = (len (f1 + f2)) + n ) ;
( n in dom g1 & n in dom g2 ) by A2, A10, XBOOLE_0:def 4;
then A11: ( g1 . n = g1 /. n & g2 . n = g2 /. n & (f1 ^ g1) . i = g1 . n & (f2 ^ g2) . i = g2 . n ) by A1, A3, A10, FINSEQ_1:def 7, PARTFUN1:def 8;
thus ((f1 + f2) ^ (g1 + g2)) . i = (g1 + g2) . n by A10, FINSEQ_1:def 7
.= (g1 /. n) + (g2 /. n) by A10, A11, FVSUM_1:21
.= ((f1 ^ g1) + (f2 ^ g2)) . i by A5, A6, A11, FVSUM_1:21 ; :: thesis: verum

end;

end;

end;

hence ((f1 + f2) ^ (g1 + g2)) . i = ((f1 ^ g1) + (f2 ^ g2)) . i ; :: thesis: verum

end;

hence (f1 + f2) ^ (g1 + g2) = (f1 ^ g1) + (f2 ^ g2) by A5, FINSEQ_1:17; :: thesis: verum