let f, g be Function of (bool the carrier of E),(bool the carrier of E); :: thesis: ( ( for A being binary-image of E holds f . A = A (+) B ) & ( for A being binary-image of E holds g . A = A (+) B ) implies f = g )

assume A3: for A being binary-image of E holds f . A = A (+) B ; :: thesis: ( ex A being binary-image of E st not g . A = A (+) B or f = g )

assume A4: for A being binary-image of E holds g . A = A (+) B ; :: thesis: f = g

assume A3: for A being binary-image of E holds f . A = A (+) B ; :: thesis: ( ex A being binary-image of E st not g . A = A (+) B or f = g )

assume A4: for A being binary-image of E holds g . A = A (+) B ; :: thesis: f = g

now :: thesis: for x being object st x in bool the carrier of E holds

f . x = g . x

hence
f = g
by FUNCT_2:12; :: thesis: verumf . x = g . x

let x be object ; :: thesis: ( x in bool the carrier of E implies f . x = g . x )

assume x in bool the carrier of E ; :: thesis: f . x = g . x

then reconsider A = x as binary-image of E ;

thus f . x = A (+) B by A3

.= g . x by A4 ; :: thesis: verum

end;assume x in bool the carrier of E ; :: thesis: f . x = g . x

then reconsider A = x as binary-image of E ;

thus f . x = A (+) B by A3

.= g . x by A4 ; :: thesis: verum