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 = dom f2 by A1, FINSEQ_3:29;
A3: dom g2 = Seg (len g2) by FINSEQ_1:def 3;
A4: dom g1 = Seg (len g1) by FINSEQ_1:def 3;
A5: dom (f1 ^ g1) = Seg ((len f1) + (len g1)) by FINSEQ_1:def 7;
A6: dom (f2 ^ g2) = Seg ((len f2) + (len g2)) by FINSEQ_1:def 7;
A7: dom (g1 + g2) = (dom g1) /\ (dom g2) by Lm1;
A8: dom (f1 + f2) = (dom f1) /\ (dom f2) by Lm1;
then A9: len (f1 + f2) = len f1 by A2, FINSEQ_3:29;
A10: dom ((f1 ^ g1) + (f2 ^ g2)) = (dom (f1 ^ g1)) /\ (dom (f2 ^ g2)) by Lm1;

A11: now :: thesis: dom ((f1 + f2) ^ (g1 + g2)) = dom ((f1 ^ g1) + (f2 ^ g2))

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

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

then Seg (len g1) c= Seg (len g2) by FINSEQ_1:5;
then dom (g1 + g2) = dom g1 by A7, A4, A3, XBOOLE_1:28;
then A13: len (g1 + g2) = len g1 by FINSEQ_3:29;
(len f1) + (len g1) <= (len f2) + (len g2) by A1, A12, XREAL_1:7;
then dom (f1 ^ g1) c= dom (f2 ^ g2) by A5, A6, FINSEQ_1:5;
then dom ((f1 ^ g1) + (f2 ^ g2)) = dom (f1 ^ g1) by A10, XBOOLE_1:28;
hence dom ((f1 + f2) ^ (g1 + g2)) = dom ((f1 ^ g1) + (f2 ^ g2)) by A9, A5, A13, FINSEQ_1:def 7; :: thesis: verum

end;

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

then Seg (len g2) c= Seg (len g1) by FINSEQ_1:5;
then dom (g1 + g2) = dom g2 by A7, A4, A3, XBOOLE_1:28;
then A15: len (g1 + g2) = len g2 by FINSEQ_3:29;
(len f1) + (len g1) > (len f2) + (len g2) by A1, A14, XREAL_1:8;
then dom (f2 ^ g2) c= dom (f1 ^ g1) by A5, A6, FINSEQ_1:5;
then dom ((f1 ^ g1) + (f2 ^ g2)) = dom (f2 ^ g2) by A10, XBOOLE_1:28;
hence dom ((f1 + f2) ^ (g1 + g2)) = dom ((f1 ^ g1) + (f2 ^ g2)) by A1, A9, A6, A15, FINSEQ_1:def 7; :: thesis: verum

end;

end;

end;

now :: thesis: for i being Nat st i in dom ((f1 + f2) ^ (g1 + g2)) holds
((f1 + f2) ^ (g1 + g2)) . i = ((f1 ^ g1) + (f2 ^ g2)) . i

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

now :: thesis: ((f1 + f2) ^ (g1 + g2)) . i = ((f1 ^ g1) + (f2 ^ g2)) . i

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

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

then A18: f2 . i = (f2 ^ g2) . i by A8, A2, FINSEQ_1:def 7;
A19: f2 /. i = f2 . i by A8, A2, A17, PARTFUN1:def 6;
A20: f1 . i = (f1 ^ g1) . i by A8, A2, A17, FINSEQ_1:def 7;
A21: f1 /. i = f1 . i by A8, A2, A17, PARTFUN1:def 6;
thus ((f1 + f2) ^ (g1 + g2)) . i = (f1 + f2) . i by A17, FINSEQ_1:def 7
.= (f1 /. i) + (f2 /. i) by A17, A21, A19, FVSUM_1:17
.= ((f1 ^ g1) + (f2 ^ g2)) . i by A11, A16, A21, A19, A20, A18, FVSUM_1:17 ; :: 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
A22: n in dom (g1 + g2) and
A23: i = (len (f1 + f2)) + n ;
A24: n in dom g1 by A7, A22, XBOOLE_0:def 4;
then A25: (f1 ^ g1) . i = g1 . n by A9, A23, FINSEQ_1:def 7;
A26: g1 . n = g1 /. n by A24, PARTFUN1:def 6;
A27: n in dom g2 by A7, A22, XBOOLE_0:def 4;
then A28: (f2 ^ g2) . i = g2 . n by A1, A9, A23, FINSEQ_1:def 7;
A29: g2 . n = g2 /. n by A27, PARTFUN1:def 6;
thus ((f1 + f2) ^ (g1 + g2)) . i = (g1 + g2) . n by A22, A23, FINSEQ_1:def 7
.= (g1 /. n) + (g2 /. n) by A22, A26, A29, FVSUM_1:17
.= ((f1 ^ g1) + (f2 ^ g2)) . i by A11, A16, A26, A29, A25, A28, FVSUM_1:17 ; :: 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 A11, FINSEQ_1:13; :: thesis: verum