consider j being Element of J;
A1: dom A = J by PARTFUN1:def 4;
reconsider U0 = A . j as Universal_Algebra ;
take signature U0 ; :: thesis: for j being Element of J holds signature U0 = signature (A . j)
let j1 be Element of J; :: thesis: signature U0 = signature (A . j1)
thus signature U0 = signature (A . j1) by A1, Def12; :: thesis: verum