let f0, f1 be Function of (product F),(product (F * a)); :: thesis: ( ( for x being Element of (product F) holds f0 . x = x * a ) & ( for x being Element of (product F) holds f1 . x = x * a ) implies f0 = f1 )
assume A5: for x being Element of (product F) holds f0 . x = x * a ; :: thesis: ( ex x being Element of (product F) st not f1 . x = x * a or f0 = f1 )
assume A6: for x being Element of (product F) holds f1 . x = x * a ; :: thesis: f0 = f1
A7: dom f1 = [#] (product F) by PARTFUN1:def 2;
for x being object st x in dom f0 holds
f0 . x = f1 . x
proof
let x be object ; :: thesis: ( x in dom f0 implies f0 . x = f1 . x )
assume x in dom f0 ; :: thesis: f0 . x = f1 . x
then reconsider x = x as Element of (product F) ;
f0 . x = x * a by A5
.= f1 . x by A6 ;
hence f0 . x = f1 . x ; :: thesis: verum
end;
hence f0 = f1 by A7, PARTFUN1:def 2; :: thesis: verum