let f be Function-yielding Function; :: thesis: for g being FinSequence
for x, y being object holds (g *. f) _ (x,y) = g . (f _ (x,y))
let g be FinSequence; :: thesis: for x, y being object holds (g *. f) _ (x,y) = g . (f _ (x,y))
let x, y be object ; :: thesis: (g *. f) _ (x,y) = g . (f _ (x,y))
A1: (g *. f) . x = g * (f . x) by Th41;

per cases ( y in dom ((g *. f) . x) or not y in dom (f . x) or not (f . x) . y in dom g ) by A1, FUNCT_1:11;

suppose y in dom ((g *. f) . x) ; :: thesis: (g *. f) _ (x,y) = g . (f _ (x,y))

hence (g *. f) _ (x,y) = g . (f _ (x,y)) by A1, FUNCT_1:12; :: thesis: verum

end;

suppose not y in dom (f . x) ; :: thesis: (g *. f) _ (x,y) = g . (f _ (x,y))

then ( not y in dom ((g *. f) . x) & (f . x) . y = {} ) by A1, FUNCT_1:11, FUNCT_1:def 2;
then ( not (f . x) . y in dom g & ((g *. f) . x) . y = {} ) by FINSEQ_3:25, FUNCT_1:def 2;
hence (g *. f) _ (x,y) = g . (f _ (x,y)) by FUNCT_1:def 2; :: thesis: verum

end;

suppose not (f . x) . y in dom g ; :: thesis: (g *. f) _ (x,y) = g . (f _ (x,y))

then ( not y in dom ((g *. f) . x) & g . ((f . x) . y) = {} ) by A1, FUNCT_1:11, FUNCT_1:def 2;
hence (g *. f) _ (x,y) = g . (f _ (x,y)) by FUNCT_1:def 2; :: thesis: verum

end;

end;