let it1, it2 be Tuple of n, BOOLEAN ; :: thesis: ( ( for i being set st i in Seg n holds
it1 . i = (p /. i) '&' (q /. i) ) & ( for i being set st i in Seg n holds
it2 . i = (p /. i) '&' (q /. i) ) implies it1 = it2 )
assume that
A4: for i being set st i in Seg n holds
it1 . i = (p /. i) '&' (q /. i) and
A5: for i being set st i in Seg n holds
it2 . i = (p /. i) '&' (q /. i) ; :: thesis: it1 = it2

now :: thesis: ( dom it1 = dom it2 & ( for x being object st x in dom it1 holds
it1 . x = it2 . x ) )

A6: dom it1 = Seg n by Lm1;
hence dom it1 = dom it2 by Lm1; :: thesis: for x being object st x in dom it1 holds
it1 . x = it2 . x
let x be object ; :: thesis: ( x in dom it1 implies it1 . x = it2 . x )
assume A7: x in dom it1 ; :: thesis: it1 . x = it2 . x
hence it1 . x = (p /. x) '&' (q /. x) by A4, A6
.= it2 . x by A5, A6, A7 ;
:: thesis: verum

end;

hence it1 = it2 by FUNCT_1:2; :: thesis: verum