let L be non empty RelStr ; :: thesis: for F, G being Function-yielding Function st dom F = dom G & ( for x being set st x in dom F holds
\\/ (F . x),L = \\/ (G . x),L ) holds
\// F,L = \// G,L
let F, G be Function-yielding Function; :: thesis: ( dom F = dom G & ( for x being set st x in dom F holds
\\/ (F . x),L = \\/ (G . x),L ) implies \// F,L = \// G,L )
assume that
A1: dom F = dom G and
A2: for x being set st x in dom F holds
\\/ (F . x),L = \\/ (G . x),L ; :: thesis: \// F,L = \// G,L
A3: for x being set st x in dom F holds
(\// F,L) . x = (\// G,L) . x

proof

let x be set ; :: thesis: ( x in dom F implies (\// F,L) . x = (\// G,L) . x )
assume A4: x in dom F ; :: thesis: (\// F,L) . x = (\// G,L) . x
hence (\// F,L) . x = \\/ (F . x),L by Def1
.= \\/ (G . x),L by A2, A4
.= (\// G,L) . x by A1, A4, Def1 ;
:: thesis: verum

end;

( dom (\// F,L) = dom F & dom (\// G,L) = dom G ) by FUNCT_2:def 1;
hence \// F,L = \// G,L by A1, A3, FUNCT_1:9; :: thesis: verum