let L be non empty RelStr ; 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; ( 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)
; /\\ (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 ;
( x in dom F implies (/\\ (F,L)) . x = (/\\ (G,L)) . x )
assume A4:
x in dom F
;
(/\\ (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
;
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; verum