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

hence /\\ (F,L) = /\\ (G,L) by A1, A3, FUNCT_1:2; :: thesis: verum

//\ ((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

( dom (/\\ (F,L)) = dom F & dom (/\\ (G,L)) = dom G )
by FUNCT_2:def 1;
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 Def2

.= //\ ((G . x),L) by A2, A4

.= (/\\ (G,L)) . x by A1, A4, Def2 ;

:: thesis: verum

end;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

hence /\\ (F,L) = /\\ (G,L) by A1, A3, FUNCT_1:2; :: thesis: verum