let F1, F2 be Function; :: thesis: ( dom F1 = (dom F) /\ (dom G) & ( for i being set st i in dom F1 holds
for f, g being FinSequence st f = F . i & g = G . i holds
F1 . i = f ^ g ) & dom F2 = (dom F) /\ (dom G) & ( for i being set st i in dom F2 holds
for f, g being FinSequence st f = F . i & g = G . i holds
F2 . i = f ^ g ) implies F1 = F2 )
assume that
A3: dom F1 = (dom F) /\ (dom G) and
A4: for i being set st i in dom F1 holds
for f, g being FinSequence st f = F . i & g = G . i holds
F1 . i = f ^ g and
A5: dom F2 = (dom F) /\ (dom G) and
A6: for i being set st i in dom F2 holds
for f, g being FinSequence st f = F . i & g = G . i holds
F2 . i = f ^ g ; :: thesis: F1 = F2

now :: thesis: for x being object st x in dom F1 holds
F1 . x = F2 . x

let x be object ; :: thesis: ( x in dom F1 implies F1 . x = F2 . x )
assume A7: x in dom F1 ; :: thesis: F1 . x = F2 . x
then ( x in dom F & x in dom G ) by A3, XBOOLE_0:def 4;
then reconsider f = F . x, g = G . x as FinSequence by Def3;
thus F1 . x = f ^ g by A4, A7
.= F2 . x by A3, A5, A6, A7 ; :: thesis: verum

end;

hence F1 = F2 by A3, A5; :: thesis: verum