let f1, f2 be Sequence; :: thesis: ( dom f1 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
f1 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
f1 . ((dom fi) +^ A) = psi . A ) & dom f2 = (dom fi) +^ (dom psi) & ( for A being Ordinal st A in dom fi holds
f2 . A = fi . A ) & ( for A being Ordinal st A in dom psi holds
f2 . ((dom fi) +^ A) = psi . A ) implies f1 = f2 )
assume that
A5: dom f1 = (dom fi) +^ (dom psi) and
A6: for A being Ordinal st A in dom fi holds
f1 . A = fi . A and
A7: for A being Ordinal st A in dom psi holds
f1 . ((dom fi) +^ A) = psi . A and
A8: dom f2 = (dom fi) +^ (dom psi) and
A9: for A being Ordinal st A in dom fi holds
f2 . A = fi . A and
A10: for A being Ordinal st A in dom psi holds
f2 . ((dom fi) +^ A) = psi . A ; :: thesis: f1 = f2
now :: thesis: for x being object st x in (dom fi) +^ (dom psi) holds
f1 . x = f2 . x
let x be object ; :: thesis: ( x in (dom fi) +^ (dom psi) implies f1 . x = f2 . x )
assume A11: x in (dom fi) +^ (dom psi) ; :: thesis: f1 . x = f2 . x
then reconsider A = x as Ordinal ;
now :: thesis: f1 . x = f2 . x
per cases ( x in dom fi or not x in dom fi ) ;
suppose A12: x in dom fi ; :: thesis: f1 . x = f2 . x
then f1 . A = fi . A by A6;
hence f1 . x = f2 . x by A9, A12; :: thesis: verum
end;
suppose not x in dom fi ; :: thesis: f1 . x = f2 . x
then dom fi c= A by ORDINAL1:16;
then A13: (dom fi) +^ (A -^ (dom fi)) = A by ORDINAL3:def 5;
then f1 . A = psi . (A -^ (dom fi)) by A7, A11, ORDINAL3:22;
hence f1 . x = f2 . x by A10, A11, A13, ORDINAL3:22; :: thesis: verum
end;
end;
end;
hence f1 . x = f2 . x ; :: thesis: verum
end;
hence f1 = f2 by A5, A8, FUNCT_1:2; :: thesis: verum