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 Def2
.= //\ (G . x),L by A2, A4
.= (/\\ G,L) . x by A1, A4, Def2 ;
:: 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