let X be BCI-algebra; :: thesis: for G being SubAlgebra of X
for K being closed Ideal of X
for RK being I-congruence of X,K holds HK G,RK is SubAlgebra of X
let G be SubAlgebra of X; :: thesis: for K being closed Ideal of X
for RK being I-congruence of X,K holds HK G,RK is SubAlgebra of X
let K be closed Ideal of X; :: thesis: for RK being I-congruence of X,K holds HK G,RK is SubAlgebra of X
let RK be I-congruence of X,K; :: thesis: HK G,RK is SubAlgebra of X
set IT = HK G,RK;
C1: 0. (HK G,RK) = 0. X ;
set V1 = the carrier of (HK G,RK);
reconsider D = the carrier of (HK G,RK) as non empty set ;
set A = the InternalDiff of X || the carrier of (HK G,RK);
set B = the InternalDiff of (HK G,RK);
set VV = the carrier of X;
dom the InternalDiff of X = [:the carrier of X,the carrier of X:] by FUNCT_2:def 1;
then ( dom (the InternalDiff of X || the carrier of (HK G,RK)) = [:the carrier of X,the carrier of X:] /\ [:the carrier of (HK G,RK),the carrier of (HK G,RK):] & [:the carrier of (HK G,RK),the carrier of (HK G,RK):] c= [:the carrier of X,the carrier of X:] ) by RELAT_1:90, ZFMISC_1:119;
then A3: dom (the InternalDiff of X || the carrier of (HK G,RK)) = [:D,D:] by XBOOLE_1:28;
rng (the InternalDiff of X || the carrier of (HK G,RK)) = D

proof

for y being set holds
( y in D iff ex z being set st
( z in dom (the InternalDiff of X || the carrier of (HK G,RK)) & y = (the InternalDiff of X || the carrier of (HK G,RK)) . z ) )

proof

let y be set ; :: thesis: ( y in D iff ex z being set st
( z in dom (the InternalDiff of X || the carrier of (HK G,RK)) & y = (the InternalDiff of X || the carrier of (HK G,RK)) . z ) )
E1: ( y in D implies ex z being set st
( z in dom (the InternalDiff of X || the carrier of (HK G,RK)) & y = (the InternalDiff of X || the carrier of (HK G,RK)) . z ) )

proof

assume F1: y in D ; :: thesis: ex z being set st
( z in dom (the InternalDiff of X || the carrier of (HK G,RK)) & y = (the InternalDiff of X || the carrier of (HK G,RK)) . z )
then reconsider y1 = y, y2 = 0. (HK G,RK) as Element of X ;
F3: ( [y,(0. (HK G,RK))] in [:D,D:] & [y,(0. (HK G,RK))] in [:the carrier of X,the carrier of X:] ) by F1, ZFMISC_1:106;
then (the InternalDiff of X || the carrier of (HK G,RK)) . [y,(0. (HK G,RK))] = y1 \ y2 by FUNCT_1:72
.= y by BCIALG_1:2 ;
hence ex z being set st
( z in dom (the InternalDiff of X || the carrier of (HK G,RK)) & y = (the InternalDiff of X || the carrier of (HK G,RK)) . z ) by A3, F3; :: thesis: verum

end;

now

given z being set such that F5: ( z in dom (the InternalDiff of X || the carrier of (HK G,RK)) & y = (the InternalDiff of X || the carrier of (HK G,RK)) . z ) ; :: thesis: y in D
consider x1, x2 being set such that
F7: ( x1 in D & x2 in D ) and
F9: z = [x1,x2] by A3, F5, ZFMISC_1:def 2;
reconsider x1 = x1, x2 = x2 as Element of Union G,RK by F7;
reconsider v1 = x1, v2 = x2 as Element of the carrier of X ;
y = v1 \ v2 by F5, F9, FUNCT_1:70;
then y = x1 \ x2 by Def6;
hence y in D ; :: thesis: verum

end;

hence ( y in D iff ex z being set st
( z in dom (the InternalDiff of X || the carrier of (HK G,RK)) & y = (the InternalDiff of X || the carrier of (HK G,RK)) . z ) ) by E1; :: thesis: verum

end;

hence rng (the InternalDiff of X || the carrier of (HK G,RK)) = D by FUNCT_1:def 5; :: thesis: verum

end;

then reconsider A = the InternalDiff of X || the carrier of (HK G,RK) as BinOp of the carrier of (HK G,RK) by A3, FUNCT_2:def 1, RELSET_1:11;

now

let x, y be Element of the carrier of (HK G,RK); :: thesis: A . x,y = the InternalDiff of (HK G,RK) . x,y
G1: ( x in the carrier of (HK G,RK) & y in the carrier of (HK G,RK) ) ;
then G3: ( [x,y] in [:the carrier of (HK G,RK),the carrier of (HK G,RK):] & [x,y] in [:the carrier of X,the carrier of X:] ) by ZFMISC_1:def 2;
reconsider xx = x, yy = y as Element of Union G,RK ;
reconsider vx = x, vy = y as Element of the carrier of X by G1;
A . x,y = vx \ vy by G3, FUNCT_1:72;
hence A . x,y = the InternalDiff of (HK G,RK) . x,y by Def6; :: thesis: verum

end;

then A = the InternalDiff of (HK G,RK) by BINOP_1:2;
hence HK G,RK is SubAlgebra of X by C1, BCIALG_1:def 10; :: thesis: verum