let L be non empty RelStr ; :: thesis: for F, G being Function-yielding Function st dom F = dom G & ( for x being object 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 object 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 object st x in dom F holds
\\/ ((F . x),L) = \\/ ((G . x),L) ; :: thesis: \// (F,L) = \// (G,L)
A3: for x being object st x in dom F holds
(\// (F,L)) . x = (\// (G,L)) . x

proof

let x be object ; :: 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:2; :: thesis: verum